Zulip Chat Archive

Stream: lean4

Topic: iterative definition


PaleChaos (Mar 21 2022 at 13:54):

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 (Mar 21 2022 at 13:59):

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 (Mar 21 2022 at 14:00):

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

PaleChaos (Mar 21 2022 at 14:13):

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 (Mar 21 2022 at 14:13):

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 (Mar 21 2022 at 14:14):

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

PaleChaos (Mar 21 2022 at 14:17):

Thank you.

Mario Carneiro (Mar 21 2022 at 18:48):

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)


Last updated: Dec 20 2023 at 11:08 UTC