leanprover-community / lean4-metaprogramming-book

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

Better intro for Expressions chapter #91

Closed JLimperg closed 1 year ago

JLimperg commented 1 year ago

As noted on Zulip, some of the phrasing in the intro of this chapter was a bit misleading. I've taken this opportunity to put some more high-level discussion in there as well.