unused let disappears

Stream: lean4

[Alexander Bentkamp]

set_option pp.all true

def pro := let x := 42; false

#print pro
-- def pro : Bool :=
-- false

Why does the let disappear when I don't use it? Can I prevent this somehow?

[Alexander Bentkamp]

Ok, I think I found the answer: I should use let_fun if I want that behavior:

def pro := let_fun x := 42; false

#print pro
/-
def pro : Bool :=
let_fun x : Nat := @OfNat.ofNat.{0} Nat 42 (instOfNatNat 42);
false
-/

[Alexander Bentkamp]

However, it would be nicer if I could produce an actual let expression that doesn't disappear...

[Gabriel Ebner]

You can write your own elaborator to do that.

[Gabriel Ebner]

Hmm, apparently this doesn't work. For some reason def removes the let binding.

#check let x := 42; false -- contains let

[Sebastian Ullrich]

Yes, I'm not sure this is intentional. The binding is still there after elaboration of the body has completed.

[Elab.definition.body] pro : Nat :=
let x := 42;
false

[Alexander Bentkamp]

I guess it's this line that removes it? https://github.com/leanprover/lean4/blob/5a8f4fd946c38441910b780003dce3f7d577bb20/stage0/src/Lean/Elab/MutualDef.lean#L633

[Sebastian Ullrich]

No, that step is before the above trace

[Leonardo de Moura]

Pushed a fix for this.

[Notification Bot]

Alexander Bentkamp has marked this topic as unresolved.

[Alexander Bentkamp]

Ok :-)

[Leonardo de Moura]

@Gabriel Ebner What is the proper way of adding a link to a Zulip thread?
BTW, I was originally linking to the thread, but I linked to a particular message in recent commits. However, it seems the link breaks in both cases when we mark the topic as resolved.

[Gabriel Ebner]

You're doing everything right, Leo. It's the resolve feature that's broken.

[Gabriel Ebner]

Resolving a thread literally changes the thread title.

[Gabriel Ebner]

And the links refer to the thread title.

[Wojciech Nawrocki]

Resurrecting this old thread, what is the purpose of let_fun? I can see that let_delayed is used in do-notation elaboration to enforce some elaboration order, but I can't tell why let_fun is needed. The difference to plain let x := v; t is that we do not get x == v as a definitional equality when checking t.

[Leonardo de Moura]

let_fun produces simpler hypotheses in our proof goals. They are of the form x : type instead of x : type := v. We use it to implement macros such as show, have, and have with patterns. I guess users will find new uses for it too. It is semantically equivalent to (fun x => t) v but the elaboration order is different.

[Leonardo de Moura]

Another potential use is representing programs with many let-decls. Most of them are probably equivalent to (fun x => t) v. Thus, eagerly converting them to let_fun may be useful, because simp can handle it more efficiently. We have seen some Coq libraries that define macros like let_fun for this reason.

[Wojciech Nawrocki]

Interesting, thank you! Using these as a kind of opaque let sounds useful.