Syntax extension and hygienic macros

Plain-language version: Programs and proofs in one language

Lean's grammar is not fixed. A Lean source file can add operators, notations and whole new syntactic forms, and say what each one means by rewriting it into syntax Lean already understands. The rewriting is done by macros, and Lean's macros are hygienic: a name that a macro introduces cannot capture a name the user wrote, and a name the user wrote cannot capture one the macro relies on. This page shows the commands, from the simplest (infixl) to the most general (macro_rules), and what hygiene prevents, with examples compiled by Lean 4.34.1. The design is set out by Ullrich and de Moura.

Where syntax extension sits

Lean reads a source file one command at a time. Each command is parsed, then elaborated into terms of the type theory, and only the elaborated result is passed to the Lean kernel. Macro expansion happens after parsing, as part of elaboration: before a piece of syntax is elaborated, any macro at its outermost layer is expanded. A macro takes a piece of syntax and returns another piece of syntax; the reference manual calls the expansion of a notation "a purely syntactic process that occurs prior to elaboration or code generation". Whatever a macro produces is then elaborated and checked exactly as if the user had typed it. A macro can change what is written; it cannot prove anything that the text it produces could not prove if typed by hand.

The commands form a tower. The operator commands are shorthands for notation. In Ullrich and de Moura's account, notation is itself a macro that generates a macro, and macro expands into a grammar rule (syntax) paired with a rewriting rule (macro_rules). In Lean 4.34.1, notation and macro are each handled by an elaborator that produces this pair directly. The syntax and macro_rules commands in turn become ordinary Lean definitions that the parser and the macro expander consult.

Operators

The smallest extension names a binary operator.

def avg (a b : Nat) : Nat := (a + b) / 2

infixl:65 " ⊞ " => avg

#eval 2 ⊞ 4 ⊞ 10
#check fun (a b : Nat) => avg a b

The #eval prints 6: the operator associates to the left, so the expression is avg (avg 2 4) 10, that is avg 3 10. The reference manual gives the expansion exactly: infixl:prec "op" => f stands for notation:prec x:prec "op" y:prec1 => f x y, where prec1 is one more than prec, so the left operand may itself be a use of the operator and the right operand may not. A custom operator must state its precedence; there is no default.

The #check shows the other direction. Asked to print avg a b, Lean prints

fun a b => a ⊞ b : Nat → Nat → Nat

The command has also generated an unexpander, a rule used when terms are displayed. A notation gets one when its right-hand side applies a named function and each of its term positions occurs there exactly once; a notation that expands to an anonymous function gets none. The operator therefore appears in goals and error messages, not only in source text.

Notation, syntax and macro rules

notation accepts any mixture of tokens and term positions, and its right-hand side is a template. When a template is not enough, the two halves can be written separately. syntax adds a grammar rule to a syntax category (here term), and macro_rules says how to rewrite it.

syntax "∑ " ident " ∈ " term ", " term : term

macro_rules
  | `(∑ $i ∈ $xs, $body) => `(List.foldl (fun acc $i => acc + $body) 0 $xs)

#eval ∑ i ∈ [1, 2, 3, 4], i * i

The output is 30, the sum of the squares of 1 to 4. The pattern on the left of => and the result on the right are syntax quotations, written `(...). Inside them $i, $xs and $body are antiquotations: holes that match syntax in a pattern and insert it in a result. A quotation produces syntax, not a term; it is parsed but not elaborated.

macro_rules is open. More rules for the same syntax may be added later, in the same file or another, and the most recently defined is tried first. A rule that does not apply hands the syntax on to the next one, by throwing the exception unsupportedSyntax; any other exception is reported as an error. Only the outermost layer of syntax is expanded at a time, and nested macros are expanded when the elaborator reaches them.

Syntax categories are not limited to terms. Commands and tactics are categories too, and a library may declare its own with declare_syntax_cat. Ullrich and de Moura give an example of why this matters: a big-operator file in Coq's Mathematical Components library repeats twelve notations for index ranges once for each of three operators, because Coq's notation system cannot abstract over the index syntax; with a category for index ranges, each range form is interpreted once and every operator reuses it.

What hygiene prevents

A macro is a function on syntax, and syntax contains names. Two kinds of accident follow from that.

The first is variable capture: a binder the macro introduces captures a name the user supplied. Ullrich and de Moura's example is a notation for constant functions.

notation "const" e => fun x => e

#check fun (x : Nat) => const x
#eval (fun (x : Nat) => const x) 1 2

Read as text substitution, const x becomes fun x => x, the identity, and the whole expression would return its second argument. Lean prints

fun x x_1 => x : (x : Nat) → ?m.2 x → Nat
1

The binder that the notation introduced has been renamed (Lean displays it as x_1), the user's x still refers to the outer binder, and the function returns its first argument. The mechanism is the macro scope. Each expansion of a macro tags every identifier it introduces with a fresh scope, and a binder and a use of a name match only if their tags agree. The user's x carries no tag and the macro's carries one, so they are different names.

Hygiene can be switched off, and the same notation then captures.

set_option hygiene false in
notation "const'" e => fun x => e

#eval (fun (x : Nat) => const' x) 1 2

This prints 2, and Lean's linter warns that the outer x is never referenced: the macro's binder has taken it. The summation notation above is protected in the same way. Its accumulator is called acc, and a user's variable of that name is not affected.

#eval let acc := 100; ∑ i ∈ [1, 2, 3], acc * i

The result is 600. Rewritten by plain substitution, the body acc * i would refer to the accumulator, which starts at 0, and the result would be 0.

The second kind of accident runs the other way: a local name at the use site captures a global name the macro relies on.

def double (n : Nat) : Nat := 2 * n

macro "dbl! " e:term : term => `(double $e)

#eval let double := fun (n : Nat) => n; dbl! 5

The output is 10, and Lean warns that the local variable double is not referenced. The identifier double in the quotation carries the macro's scope and the local binding at the use site does not, so the two do not match. When the quotation `(double $e) was compiled, the name was also resolved to the global function and recorded with it, so a global of the same name introduced later cannot redirect it either.

Hygiene in tactics

Tactics form a syntax category, so a tactic can be a macro (the tactic framework treats the result like any other tactic). This one introduces a hypothesis and uses it.

macro "intro_assumption" : tactic => `(tactic| (intro h; exact h))

example (p : Prop) : p → p := by intro_assumption

The proof is accepted. The name h, however, belongs to the macro. A script that uses a macro to introduce h and then refers to h itself fails.

macro "intro_hyp" : tactic => `(tactic| intro h)

example (p : Prop) : p → p := by
  intro_hyp
  exact h

Lean reports Unknown identifier `h` at the last line. The hypothesis exists, but under a name the user cannot type:

macro "intro_hyp" : tactic => `(tactic| intro h)

example (p : Prop) : p → p := by
  intro_hyp
  trace_state
  assumption

p : Prop
h✝ : p
⊢ p

The dagger marks an inaccessible name, and assumption, which does not need the name, closes the goal. Ullrich and de Moura report that Lean 3's tactic quotations had both faults: a short tactic script for injectivity lemmas broke when it was used from a library for homotopy type theory that defined its own propext and Iff.intro, and scripts could refer to names a tactic had introduced. They describe Lean 4's tactic language as, to their knowledge, the first in an established theorem prover to be hygienic automatically in this sense.

Mathematics in its own notation

Mathematics is written in notation that varies by field and by author, and much of it binds variables: sums, products, integrals, set-builder notation, quantifiers over a finite set. A fixed grammar forces a formal text away from that notation. Lean's macros let a library add it, with three properties that matter in practice.

Binding notation is safe to define. A notation that introduces its own bound variables, such as the sum above, does not interfere with the names its user chooses, and the user need not know which names it uses inside. Without hygiene, every such notation would be a hazard of the kind shown in the const example.

Notation is printed back. Because an unexpander is generated where possible, goals and error messages show the notation the reader wrote, not the function it stands for.

Notation can be confined. A notation marked scoped is active only where its namespace is open, so a field's notation need not occupy the grammar of every other field.

def avg (a b : Nat) : Nat := (a + b) / 2

namespace Averages
scoped infixl:65 " ⊞ " => avg
end Averages

open Averages in
#eval 2 ⊞ 4 ⊞ 10

This prints 6. Without the open, ⊞ is not part of the grammar:

def avg (a b : Nat) : Nat := (a + b) / 2

namespace Averages
scoped infixl:65 " ⊞ " => avg
end Averages

#check (2 ⊞ 4 : Nat)

Lean stops at the operator with the parse error expected token.

What notation does not do is add meaning. It changes how a statement is written and read, and nothing that the Lean kernel checks. That is also its risk. A statement that uses unfamiliar notation may not say what it appears to say, and the reference manual's guidance on validating a proof names custom notation among the things to investigate when there is doubt that a theorem states what was intended.

A macro sees only syntax. When a translation depends on types, for example on whether an argument is a natural number or a set, a macro cannot decide it, and an elaborator is needed: a Lean program that runs inside the elaborator and constructs terms directly.

Next

Metaprogramming in Lean shows how elaborators and tactics are written as Lean programs. Monads and do-notation describes a piece of syntax that Lean translates into ordinary terms: the do block.