A Lean 4 Metaprogramming Book

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

A PDF is available here for download (and is rebuilt on each change).

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

Sources to extract material from:

• Material written by Ed

Contributing

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.

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 --.

To open the PR, select dev as the target branch.

Building the markdown files

This is not required, but if you want to build the markdown files, you can do so by running lake run build. It requires having Python installed, as well as the lean2md package.

Or, if you have viper installed and a linked environment that has lean2md, you can call lake run viper_build.