Zulip Chat Archive

Stream: lean4

Topic: LocalDecl.value vs. toExpr


Jireh Loreaux (Oct 03 2023 at 22:03):

What's the distinction between docs#Lean.LocalDecl.value and docs#Lean.LocalDecl.toExpr ? Is one preferred, and if so, why?

Adam Topaz (Oct 03 2023 at 22:15):

The value is for let declarations.

Adam Topaz (Oct 03 2023 at 22:15):

You will get a panic if you try to use it for a non-let local decl

Adam Topaz (Oct 03 2023 at 22:16):

toExpr gives the expression associated to the fvar

Jireh Loreaux (Oct 03 2023 at 22:56):

Aha, thanks!


Last updated: Dec 20 2023 at 11:08 UTC