A Lean 4 Metaprogramming Book

Authors: Arthur Paulino, Edward Ayers, Henrik Böving, Jannis Limperg, Siddhartha Gadgil, Siddharth Bhat

• Main
  1. Introduction
  2. Expressions
  3. MetaM
  4. Syntax
  5. Elaboration
  6. Macros
  7. DSLs
  8. Tactics
• Extra
  1. Options
  2. Attributes
  3. Pretty Printing

Sources to extract material from:

• Material written by Ed

Collaborating

The markdown files are generated automatically via lean2md. Thus, if you're going to write or fix content for the book, please do so in the original Lean files inside the lean directory.

To build the markdown files, please run lake script run build

Important: since lean2md is so simple, please avoid using comment sections in Lean code blocks with /- ... -/. If you want to insert commentaries, do so with double dashes --.