Skip to main content

Documentation Index

Fetch the complete documentation index at: https://mintlify.com/leanprover/lean4/llms.txt

Use this file to discover all available pages before exploring further.

Macros are the lightest-weight metaprogramming tool in Lean 4. They operate purely on Syntax trees — no types, no environment — and are processed before elaboration begins. Because macros are hygienic and composable, they are the right tool for notation, syntactic sugar, and lightweight domain-specific languages.

​
The MacroM Monad

Every macro runs in MacroM, a stripped-down monad that provides:
  • Hygiene: fresh name generation via macro scopes (withFreshMacroScope).
  • Error reporting: Macro.throwError and Macro.throwErrorAt.
  • Exception: Macro.Exception.unsupportedSyntax to signal that this rule doesn’t handle the input (allowing fallthrough to the next rule).
MacroM deliberately does not have access to the Environment or type information. This keeps macros fast and compositional. 
-- MacroM is a simple monad alias
-- abbrev MacroM := ReaderT Macro.Context (EStateM Macro.Exception Macro.State)

​
macro_rules: Pattern-Matching Macros

macro_rules lets you write a collection of syntax-to-syntax rewrite rules. Each alternative is tried in order; on a match the rule fires and produces new syntax that re-enters macro expansion. 
-- A simple unless macro (inverts the condition of an if)
macro_rules
  | `(unless $cond do $body) => `(if !$cond then $body)
Multiple alternatives can handle different arities or shapes: 
macro_rules
  | `(myAssert $e)           => `(if !$e then panic! "Assertion failed")
  | `(myAssert $e, $msg:str) => `(if !$e then panic! $msg)
If no alternative matches, macro_rules automatically throws Macro.Exception.unsupportedSyntax, which tells the elaborator to try the next registered macro for this syntax kind.

​
macro: The Shorthand Form

For single-rule macros with a fixed syntactic form, the macro command combines syntax declaration and rule in one: 
-- macro <pattern> : <category> => <rhs>
macro "swap!" x:ident "," y:ident : term =>
  `(let tmp := $x; $x := $y; $y := tmp)
The right-hand side must be a single term (or tactic block). Internally, macro desugars to a syntax declaration followed by a macro_rules rule — you can see this by inspecting the generated code with set_option pp.all true. 
-- A do-element macro
macro "repeat" n:num "times" body:doSeq : doElem =>
  `(doElem| for _i in List.range $n do $body)

​
Syntax Quotation

Syntax quotation is the primary way to construct and deconstruct Syntax values. Backtick-paren notation `(…) lifts Lean source text into a Syntax value at compile time.

​
Building Syntax

-- Build a function application
def mkAddSyntax (a b : Syntax) : MacroM Syntax :=
  `($a + $b)

-- Build a tactic sequence
def mkRflTactic : MacroM Syntax :=
  `(tactic| rfl)

-- Build a command
def mkDefSyntax (name val : Syntax) : MacroM Syntax :=
  `(def $name := $val)
The category is inferred from context. You can specify it explicitly with `(term| …), `(tactic| …), `(command| …), etc.

​
Pattern Matching on Syntax

Syntax quotation works in patterns too: 
macro_rules
  | `(foo $x $y) => do
    -- x and y are bound as Syntax values here
    `($x + $y)

​
Antiquotation: Splicing Values In

Antiquotation (the $ escape) lets you splice a Syntax value into a quotation.
NotationMeaning
$xSplice the syntax variable x
$(e)Splice the expression e (evaluated at macro-expansion time)
$x,*Splice a comma-separated list from an array x
$x:identMatch/splice with a category annotation
$[$xs]*Splice an array of syntax nodes with no separator
$[$xs],*Splice an array with comma separators
-- Splicing an array with separators
macro "tuple" xs:term,* : term => `(($xs,*))
-- tuple 1, 2, 3  →  (1, 2, 3)

-- Splicing with explicit expression
macro "doubled" n:num : term =>
  let v := n.getNat * 2
  `($(Syntax.mkNumLit (toString v)))

​
Hygienic Macros and Auto-Generated Names

Lean 4 macros are hygienic by default. When a macro introduces a new binding, it gets a fresh macro scope suffix that prevents capture of variables from the call site. 
-- This is safe: `tmp` won't accidentally capture a user variable named `tmp`
macro "swap!" x:ident "," y:ident : tactic =>
  `(tactic|
    (let tmp := $x
     $x := $y
     $y := tmp))
Under the hood, tmp becomes something like tmp@[macro_scope_42]. The surface syntax still shows tmp in error messages, but the kernel sees the scoped name. If you want to intentionally capture a name (anti-hygienic), use mkIdent without a fresh scope: 
-- Explicitly introduce a name that is visible at the call site
macro "withX" body:term : term =>
  let x := mkIdent `x
  `(let $x := 42; $body)
Anti-hygienic macros can cause confusing errors. Prefer hygienic macros unless you specifically need to introduce a name visible at the call site.

​
Error Reporting in MacroM

macro_rules
  | `(myMacro $x) => do
    if x.isNone then
      Macro.throwErrorAt x "myMacro requires a non-empty argument"
    `(doSomethingWith $x)
Use Macro.throwError for errors not tied to a specific syntax node, and Macro.throwErrorAt stx msg to attach the error to a source range.

​
Complete Example: unless and swap!

import Lean

-- unless: conditional with inverted test
macro_rules
  | `(unless $cond:term do $body:doSeq) =>
    `(if !$cond then do $body)

-- swap!: exchange two mutable variables
macro "swap!" x:ident "," y:ident : tactic =>
  `(tactic|
    (have _tmp := $x
     $x := $y
     $y := _tmp))

-- Test unless
def testUnless : IO Unit := do
  let x := 3
  unless x > 10 do
    IO.println "x is not greater than 10"

-- Test swap! in a proof context (using local variables)
example (a b : Nat) (h : a = 1) (h2 : b = 2) : True := by
  swap! a, b   -- swaps the bindings (demonstrative)
  trivial

​
Notation: Operators and Mixfix

For operator-like syntax, the notation, infixl, infixr, prefix, and postfix commands are thin wrappers around macro: 
-- Custom infix operator (left-associative, precedence 65)
infixl:65 " |> " => Function.comp   -- already in stdlib, shown for demo

-- Custom notation with multiple tokens
notation:50 a " ≈[" ε "]≈ " b => abs (a - b) < ε

-- Prefix operator
prefix:75 "↑↑" => Nat.succ ∘ Nat.succ

-- Postfix
postfix:100 "!" => Nat.factorial
Precedence numbers follow Lean’s standard: + is 65, * is 70, function application is 1024. Higher numbers bind tighter. 
-- notation supports more complex patterns
notation:10 "∀ " x " ∈ " s ", " p => ∀ x, x ∈ s → p

​
The @[macro myMacroName] Attribute

The @[macro k] attribute on a Macro function registers it as a handler for the syntax node kind k, exactly as macro_rules does internally: 
-- Low-level registration (macro_rules is preferred)
@[macro myLang.myKeyword]
def myKeywordMacro : Macro
  | `(myKeyword $x) => `(handleMyKeyword $x)
  | _ => Macro.throwUnsupported
Multiple macros registered for the same kind form a priority chain. The one with the highest priority fires first; if it throws unsupportedSyntax, the next one is tried.
Always use macro_rules or macro instead of @[macro] directly unless you need explicit control over the auxiliary definition name or priority.

Build docs developers (and LLMs) love

Get started for freeTalk to us