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