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

Published 20 hours ago • verified publisher icon leanprover-community

typo in MetaM chapter

Open Seasawher opened this issue 1 year ago • 0 comments
trafficstars

[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

Seasawher avatar Jun 15 '24 12:06 Seasawher