leanprover-community / lean4-metaprogramming-book

https://leanprover-community.github.io/lean4-metaprogramming-book/
Apache License 2.0
213 stars 53 forks source link

`let x := v in b` syntax #135

Open Seasawher opened 6 months ago

Seasawher commented 6 months ago

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.