lean4-metaprogramming-book icon indicating copy to clipboard operation
lean4-metaprogramming-book copied to clipboard

`let x := v in b` syntax

Open Seasawher opened this issue 3 months ago • 0 comments

at Expressions

letE n t v b is a let binder (let ($n : $t) := $v in $b).

I don't think there is a syntax for let followed by in.

Seasawher avatar Mar 23 '24 12:03 Seasawher