Information on Lean 4's macro system is currently scattered between a number of resources, and most of the core APIs are still undocumented. This guide consolidates some of the information and includes more practical guidance on use, leaving the really low level details to the official paper and its supplement.

The offical paper describing the mechanics behind Lean 4's macro system can be found in [Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages](https://arxiv.org/abs/2001.10490) by Sebastian Ullrich and Leonardo de Moura, and the accompanying repo with example code can be found in the paper's code [supplement](https://github.com/Kha/macro-supplement). The supplement also includes a working implementation of the macro expander, so it's a good case study for people interested in the details.

A macro is a function that takes in a syntax tree and produces a new syntax tree. Macros are useful for many reasons, but two of the big ones are a) allowing users to extend the language with new syntactic constructs without having to actually expand the core language, and b) allowing users to automate tasks that would otherwise be extremely repetitive, time-consuming, and/or error-prone.

A motivating example is Mathlib 4's set builder notation. We would like to be able to write the set of natural numbers 0, 1, and 2 as just `{0, 1, 2}`. However, Lean does not natively support this syntax, and the actual definition of a set in Mathlib does not let us just declare sets in this manner; naively using the set API would force us to write `Set.insert 1 (Set.insert 2 (Set.singleton 3))`. Instead, we can teach Lean's macro system to recognize `{0, 1, 2}` as a shorthand for a composition of existing methods and let it do the repetitive work of creating the `Set.insert...` invocation for us. In this way, we can have our more readable and more convenient syntax without having to extend Lean itself, and while retaining the simple insert/singleton API.

The general procedure is as follows:

1. Lean parses the actual code in a given file, creating a Lean AST which contains any unexpanded macros.

2. Lean repeats the cycle (elaboration ~> (macro hygiene and expansion) ~> elaboration...)

The cycle in step 2 repeats until there are no more macros which need to be expanded, and elaboration can finish normally. This repetition is required since macros can expand to other macros, and may expand to code that needs information from the elaborator. As you can see, the process of macro parsing and expansion is interleaved with the parsing and elaboration of non-macro code.

By default, macros in Lean are hygienic, but hygiene can be disabled with the option `set_option hygiene false`. Readers can learn more about hygiene and how it's implemented in the official paper and supplement linked at the top of this guide.

In the big picture, a macro has two components that must be implemented by the user, parsers and syntax transformers, where the latter is a function that says what the input syntax should expand to. There is a third component, syntax categories, such as `term`, `tactic`, and `command`, but declaring a new syntax category is not always necessary. When we say "parser" in the context of a macro, we refer to the core type `Lean.ParserDescr`, which parses elements of type `Lean.Syntax`, where `Lean.Syntax` represents elements of a Lean syntax tree. Syntax transformers are functions of type `Syntax -> MacroM Syntax`. Lean has a synonym for this type, which is simply `Macro`. `MacroM` is a monad that carries state needed for macro expansion to work nicely, including the info needed to implement hygiene.

As an example, we again refer to Mathlib's set builder notation:

This example should also make clear the reason why macros (and pretty much all of Lean 4's metaprogramming facilities) are functions that take an argument of type `Syntax` e.g. `Syntax -> MacroM Syntax`; the leading syntax element is the thing that actually triggers the macro expansion by matching with the declared parser, and as a user, you will almost always be interested in inspecting and transforming that initial syntax element (though there are cases in which it can just be ignored, as in the exfalso tactic).

Returning briefly to the API provided by Lean, `Lean.Syntax`, is pretty much what you would expect a basic syntax tree type to look like. This is a slightly simplified representation which omits details in the `atom` and `ident` constructors; users can create atoms and idents which comport with this simplified representation using the `mkAtom` and `mkIdent` methods provided in the `Lean` namespace.

For those interested, `MacroM` is a `ReaderT` with the following components:

As a review/checklist, the three (somtimes only two depending on whether you need a new syntax category) components users need to be concerned with are:

0. You may or may not need to declare a new syntax category using `declare_syntax_cat`

1. Declare a parser with either `syntax` or `macro`

2. Declare an expansion/syntax transformer with either `macro_rules` or `macro`

Parsers and syntax transformers can be declared manually, but use of the pattern language and `syntax`, `macro_rules`, and `macro` is recommended.

`declare_syntax_cat` declares a new syntax category, like `command`, `tactic`, or mathlib4's `binderterm`. These are the different categories of things that can be referred to in a quote/antiquote. Under the hood, `declare_syntax_cat` just declares a parser descriptor:

Declaring a new syntax category like this one automatically declares a quotation operator `` `(binderterm| ...)``. These pipe prefixes `<thing>|` are used in syntax quotations to say what category a given quotation is expected to be an element of. The pipe prefixes are *not* used for elements in the `term` and `command` categories (since they're considered the default), but need to be used for everything else.

Internally, elements of type `Lean.ParserDescr` are implemented as parser combinators. However, Lean offers the ability to write parsers using the macro/pattern language by way of the `syntax` keyword. This is the recommended means of writing parsers. As an example, the parser for the `rwa` (rewrite, then use assumption) tactic is:

Literals are written as double-quoted strings (`"rwa "` expects the literal sequence of characters `rwa`, while the trailing space provides a hint to the formatter that it should add a space after `rwa` when pretty printing this syntax); `rwRuleSeq` and `location` are themselves `ParserDescr`s, and we finish with `: tactic` specifying that the preceding parser is for an element in the `tactic` syntax category. The parentheses around `(location)?` are necessary (rather than `location?`) because Lean 4 allows question marks to be used in identifiers, so `location?` is one single identifier that ends with a question mark, which is not what we want.

The name `tacticRwa__` is automatically generated. You can name parser descriptors declared with the `syntax` keyword like so:

Available quantifiers are `?` (one or zero occurrences, see note below), `*` (zero or more occurrences), and `+` (one or more occurrences).

Keep in mind that Lean makes `?` available for use in identifiers, so if we want a parser to look for an optional `location`, we would need to write `(location)?` with parenthesis acting as a separator, since `location?` would look for something under the identifier `location?` (where the `?` is part of the identifier).

Parentheses can be used as delimiters.

Separated lists can be constructed like so: `$ts,*` for a comma separated list.

"extended splices" can be constructed as `$[..]`. See the official paper (p. 12) for more details.

Literals are written as double-quoted strings. A literal may use trailing whitespace (see e.g. the `rwa` or `introv` tactics) to tell the pretty-printer how it should be displayed, but such whitespace will not prevent a literal with no trailing whitespace from matching. "The spaces are relevant, but not interpreted literally. When the ParserDescr is turned into a Parser, the actual token matcher [uses the .trim of the provided string](https://github.com/leanprover/lean4/blob/master/src/Lean/Parser/Basic.lean#L1193), but the generated formatter [uses the spaces as specified](https://github.com/leanprover/lean4/blob/master/src/Lean/PrettyPrinter/Formatter.lean#L328), that is, turning the atom "rwa" in the syntax into the string rwa as part of the pretty printed output."

`macro_rules` lets you declare expansions for a given `Syntax` element using a syntax simlar to a `match` statement. The left-hand side of a match arm is a quotation (with a leading `<cat>|` for categories other than `term` and `command`) in which users can specify the pattern they'd like to write an expansion for. The right-hand side returns a syntax quotation which is the output the user wants to expand to.

A feature of Lean's macro system is that if there are multiple expansions for a particular match, Lean will try the most recently declared expansion first, and will retry with other matching expansions if the previous attempt failed. This is particularly useful for tactics.

The following example shows both the retry behavior, and the fact that macros declared using the shorthand `macro` syntax can still have additional expansions declared with `macro_rules`. This `transitivity` tactic is implemented such that it will work for either Nat.le or Nat.lt. The Nat.lt version was declared "most recently", so it will be tried first, but if it fails (for example, if the actual term in question is Nat.le) the next potential expansion will be tried:

To see the desugared definition of the actual expansion, we can again use `set_option trace.Elab.definition true in` and observe the output of the humble `exfalso` tactic defined in Mathlib4:

We can view the expansion of the parser:

Finally, we can view the expansion of the syntax transformer:

`macro` is a shortcut which allows users to declare both a parser and an expansion at the same time as a matter of convenience. Additional expansions for the parser generated by the `macro` invocation can be added with a separate `macro_rules` block (see the example in the `macro_rules` section).

TODO; for now, see the unexpander in Mathlib.Set for an example.

The [Tactic.Basic](https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/Basic.lean) file in Mathlib4 contains many good examples to learn from.

You can observe the output of commands and functions that in some way use the macro system by setting this option to true : `set_option trace.Elab.definition true`

Lean 4 also offers the option of limiting the region in which option is set with the syntax `set_option ... in`):

Hygiene can be disabled with the command option `set_option hygiene false`