Stream: MetaCoq

Topic: Lean meta programming


view this post on Zulip Bas Spitters (Mar 31 2024 at 18:25):

I've heard some very positive stories about lean's metaprogramming. Has anyone tried to make a comparison with metacoq?

view this post on Zulip Joomy Korkut (Apr 01 2024 at 14:33):

Here's my take on this, people who are more familiar with Lean's metaprogramming system (and MetaCoq) should correct me if I'm wrong. I read some of the Metaprogramming in Lean 4 book ( https://leanprover-community.github.io/lean4-metaprogramming-book/ ), and I'm familiar with Idris 1's metaprogramming system, which Lean's metaprogramming was inspired by at some point.

MetaCoq has one monad (TemplateMonad) for code inspection and generation, while Lean has many:

Also, Lean's syntax type has primitive support for syntax literals and syntax patterns. This means you don't have to use the syntax AST to match on a syntax value, you can use the surface syntax to construct syntax patterns. And you can quote/unquote syntax objects using the surface syntax. MetaCoq has notations (using the primitive tactic) that can do these, but if I remember right, it has problems with non-top-level usage.

view this post on Zulip Bas Spitters (Apr 01 2024 at 15:06):

Thanks @Joomy Korkut that's a very useful overview.


Last updated: Jul 23 2024 at 20:01 UTC