lean4-metaprogramming-book
lean4-metaprogramming-book copied to clipboard
`let x := v in b` syntax
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
.