iterative definition

Stream: lean4

[PaleChaos]

Hello, I recently started learning lean.
I have a question about the following construct, based on previous programming experience:

let mut g := #[]
for x in xs do
g := g.push(fun () => x)

this construction in lean should work, but does not work, or it should not work? Or maybe it works (I didn't manage to do it), but not correctly?

[Henrik Böving]

def foo (xs : Array Nat) : Array Nat := Id.run do -- this is important
  let mut g := #[]
  for x in xs do
    g := g.push x
  g

just works

[Henrik Böving]

Or do you already know about the do notation stuff and there is some different error?

[PaleChaos]

Henrik Böving said:

Or do you already know about the do notation stuff and there is some different error?

I want to ask if there are any problems in lean using a list of functions declared inside the loop and depending on the value of the loop variable, outside the loop?

[Henrik Böving]

Ah no, that's not an issue, you just hit a special case where the type checker cant automagically figure out what to do:

def foo (xs : Array Nat) : Array (Unit -> Nat) := Id.run do -- this is important
  let mut g := #[]
  for x in xs do
    g := g.push (fun () => x : Unit -> Nat)
  g

works

[Henrik Böving]

This is related to some universe polymorphism not working out automatically here

[PaleChaos]

Thank you.

[Mario Carneiro]

It also looks like an error in elaboration order, since you can insert by exact before the function to solve the problem. (submitted a minimized version as lean4#1058)