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.

Lean 4 is built on a tight feedback loop between its object language and its meta-language — they are the same language. Every feature you use to write proofs and programs is also available for writing the tools that process proofs and programs. Macros, custom syntax, elaborators, tactics, attributes, and linters are all first-class citizens defined in ordinary Lean 4 files.

​
What Is Metaprogramming in Lean 4?

Metaprogramming in Lean 4 means writing Lean code that runs during compilation to transform, generate, or inspect other Lean code. The system provides several distinct layers, each with a well-defined scope of authority:
  • Macros perform purely syntactic rewriting. They see Syntax trees and produce Syntax trees, with no access to types or the environment.
  • Elaborators convert Syntax into typed Expr terms, resolving names, inferring types, and discharging type-class obligations.
  • Tactics are elaborators that operate on a proof state — a list of metavariable goals — and reduce them toward Expr witnesses.
  • Attributes and linters run after type-checking to annotate declarations or report diagnostics.
These layers are stacked. A macro can expand into syntax that contains tactic blocks. A tactic can call MetaM operations for unification. An attribute handler runs in CoreM with full access to the finalized environment.

​
The Monad Stack

Lean 4’s metaprogramming API is organized as a tower of monads, each extending the one below it: 
CoreM  ←  MetaM  ←  TermElabM  ←  TacticM
Each level inherits all capabilities of the levels below it and adds new ones.

​
CoreM — Environment and Options

CoreM is the foundation. It provides:
  • getEnv / setEnv — read and write the global Environment (the store of all declarations, axioms, and kernel-checked terms).
  • getOptions — access compiler options (e.g., set_option values).
  • Tracing — trace, logInfo, logWarning, throwError.
  • Name generation — fresh names via the NameGenerator.
  • Macro scopes — withFreshMacroScope for hygienic name creation.
open Lean in
def showDeclType (name : Name) : CoreM Unit := do
  let env ← getEnv
  match env.find? name with
  | some ci => logInfo m!"Type of {name}: {ci.type}"
  | none    => throwError "declaration {name} not found"

​
MetaM — Unification and Type Inference

MetaM extends CoreM with:
  • A metavariable context (MetavarContext) tracking unification variables.
  • isDefEq — definitional equality / unification.
  • whnf — weak-head normal form reduction.
  • inferType — compute the type of an Expr.
  • mkFreshExprMVar — allocate a fresh metavariable.
  • Local contexts (LocalContext) for free variables introduced during elaboration.
  • forallTelescope, lambdaTelescope — decompose binder chains.
open Lean Meta in
def checkDefEq (t s : Expr) : MetaM Bool := do
  isDefEq t s

​
TermElabM — Term Elaboration

TermElabM extends MetaM with everything needed to elaborate surface-syntax terms:
  • Pending synthetics — collecting type-class constraints for later resolution.
  • elabTerm — the main entry point for term elaboration.
  • withLocalDecl / withLocalDeclD — introduce local variables.
  • Postponement — tactics that need more information can postpone synthesis.
  • Info trees — collecting semantic information for the language server (go-to-definition, hover, etc.).
open Lean Elab Term in
def myTermElab (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do
  let e ← elabTerm stx[1] expectedType?
  return e

​
TacticM — Proof State Manipulation

TacticM extends TermElabM with:
  • A list of open goals (List MVarId), each a metavariable representing an unsolved subgoal.
  • getGoals / setGoals — inspect and replace the goal list.
  • replaceMainGoal — replace the current main goal with zero or more new ones.
  • liftMetaTactic — bridge from MetaM into TacticM.
open Lean Elab Tactic in
def myTactic : TacticM Unit := do
  let goals ← getGoals
  logInfo m!"Current goal count: {goals.length}"

​
Macro Expansion vs Elaboration vs Compilation

Understanding when each phase runs is critical:
1

Parsing

The source file is parsed into a Syntax tree. No name resolution, no type information.
2

Macro Expansion

macro_rules and macro handlers rewrite Syntax → Syntax repeatedly until a fixpoint. Runs in MacroM, a restricted monad with no environment access. Hygiene is enforced by macro scopes.
3

Elaboration

elab_rules and term/command elaborators convert expanded Syntax into Expr. Names are resolved, types are inferred, metavariables are unified. Tactics run here as well.
4

Kernel Checking

The Lean kernel independently verifies the Expr produced by elaboration. This is a small, trusted checker that does not run user code.
5

Compilation

Verified Expr terms are compiled to IR and then to native code or interpreted bytecode. Attributes with applicationTime := .afterCompilation fire here.

​
When to Use Macros vs Elaborators

  • Your transformation is purely syntactic — no type information needed.
  • You want to define new notation that desugars to existing constructs.
  • You need lightweight combinators like unless, swap!, or custom do-notation.
  • You want maximum performance (macros are cheaper than elaborators).
  • Example: macro "myIf" c:term "then" t:term "else" e:term : term => \(ite cc t $e)`
  • You need access to the expected type, the local context, or the environment.
  • You’re defining a construct where the shape of output depends on types.
  • You need to report structured type errors.
  • You want to generate auxiliary declarations, instances, or simp lemmas.
  • Example: a deriving handler, a #check-like command, or a decide-like tactic.
  • You are producing a proof term by operating on goals.
  • You want to compose with existing tactic infrastructure (simp, exact, ring).
  • Example: a custom discharger, a domain-specific solver, or an automation combinator.

​
Further Reading

Macros

macro, macro_rules, syntax quotation, antiquotation, and operator notation.

Syntax Extensions

Defining new parsers with syntax, elab, and elab_rules.

Elaboration

Working with TermElabM, MetaM, CoreM, Expr, and the environment.

Tactic Writing

Building custom tactics with TacticM, goals, and liftMetaTactic.

Attributes & Linters

Custom attributes with AttributeImpl and linters with addLinter.

Build docs developers (and LLMs) love

Get started for freeTalk to us