leanprover-community / lean4-metaprogramming-book

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

`#h` does not work #133

Closed Seasawher closed 4 months ago

Seasawher commented 4 months ago

in 2. overview

To give a more concrete example, imagine we're implementing a #help command, that can also be written as #h.

h does not work!