leanprover-community / lean4-metaprogramming-book

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

Macro for `\mapsTo` in introduction #65

Closed siddhartha-gadgil closed 2 years ago

siddhartha-gadgil commented 2 years ago

I have added this as the first example because it is easy and people want to do this.