reference manual on `meta`

Stream: new members

[Chris M]

The reference manual says that the meta keyword is described in chapter 7. However, chapter 7 is completely unwritten. Is there a resource on these things elsewhere?

[Bryan Gin-ge Chen]

The Hitchhiker's guide to logical verification (see links here) has a few good chapters on metaprogramming in Lean.

[Scott Morrison]

There's also https://leanprover.github.io/papers/tactic.pdf

[Scott Morrison]

and reading lots of source code. :-)