search

leanprover-community / lean4-metaprogramming-book

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

typo in MetaM chapter #141

Open Seasawher opened 1 month ago

Seasawher commented 1 month ago

[Constructing Expressions] Create expression fun x, 1 + x in two ways: a) not idiomatically, with loose bound variables b) idiomatically. In what version can you use Lean.mkAppN? In what version can you use Lean.Meta.mkAppM?

it should be fun x => 1 + x