metam: extend sections on (de)constructing Exprs

leanprover-community / lean4-metaprogramming-book

https://leanprover-community.github.io/lean4-metaprogramming-book/

Apache License 2.0

211 stars 50 forks source link

metam: extend sections on (de)constructing Exprs #57

Closed JLimperg closed 2 years ago

JLimperg commented 2 years ago

I've rewritten some of the mkAppM and mkAppOptM stuff. Should be clearer now. I wasn't very happy with the mkAppOptM exposition myself, so thanks for pushing me on this. ;)