search

leanprover-community / lean4-metaprogramming-book

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

A chapter on pretty printing #11

Closed hargoniX closed 2 years ago

hargoniX commented 2 years ago

I added a new folder "optional" where things that are merely optional but not required to perform metaprogramming are stored, I moved the options chapter there since its in a good shape already anyways and added one on pretty printing, focusing especially on delaborators and unexpanders.