Zulip Chat Archive

Stream: new members

Topic: reference manual on `meta`


view this post on Zulip Chris M (Jun 29 2020 at 09:07):

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?

view this post on Zulip Bryan Gin-ge Chen (Jun 29 2020 at 09:11):

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

view this post on Zulip Scott Morrison (Jun 29 2020 at 09:48):

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

view this post on Zulip Scott Morrison (Jun 29 2020 at 09:48):

and reading lots of source code. :-)


Last updated: May 14 2021 at 00:42 UTC