Elaboration

Plain-language version: What a proof assistant does· When Lean says no

Lean theorem prover: map
Reading the edition Three levels of reading Glossary Notation Chronology
Reading by level Start here: What a proof assistant does The type theory: Terms, types and judgments How Lean works: Elaboration The history: Automath The applications: Research mathematics
Sources Sources Bibliography Further reading
Related The move to Lean

Elaboration is the step that turns what a person types into a term of Lean's core type theory. The typed text leaves out a great deal: the types of arguments, the instances behind notation such as +, conversions between number types, universe levels. The elaborator supplies all of it and produces a fully explicit term. That term then goes to the Lean kernel, which checks it. The elaborator's own reasoning is not trusted. This page follows a term from text to the Lean kernel and shows, with Lean 4.34.1's own output, what the elaborator adds.

From text to the Lean kernel

Lean processes a source file one command at a time. Each command is parsed, then elaborated, and a new definition or theorem is checked by the Lean kernel and recorded in Lean's environment, its table of definitions and theorems. Each command can change how later commands are read, since a command may add new syntax.

The parser turns characters into a syntax tree of type Syntax. The reference manual describes it as a recursive-descent parser that uses dynamic tables based on Pratt parsing, and its tables can be extended by any command. A syntax tree records what was written, not what it means: x + 1 parses the same whether x is a natural number, an integer or a matrix.

The elaborator gives the tree its meaning. Term elaborators, in the manual's words, map syntax and an optional expected type to a core language expression, and they work in a setting that provides unification, type class instance synthesis and type checking. The result is an Expr, the same data type the Lean kernel checks.

Macro expansion

Much of Lean's notation is defined by macros: rules that rewrite one piece of syntax into another before it is given meaning. Macro expansion is not a separate pass. It is interleaved with elaboration. In Lean 4.34.1 the main elaboration loop first asks whether a macro applies to the syntax at hand; if one does, it elaborates the expansion instead, and only otherwise does it call an elaboration function registered for that kind of syntax. The trace option trace.Elab.step prints each step together with the expected type at that point:

set_option trace.Elab.step true in
#check (3 : Nat) ≠ 4

3 ≠ 4 : Prop
[Elab.step] ✅️ expected type: <not-available>, term
    (3 : Nat) ≠ 4
  [Elab.step] ✅️ expected type: <not-available>, term
      binrel% Ne✝ (3 : Nat) 4
    [Elab.step] ✅️ expected type: <not-available>, term
        (3 : Nat)
      [Elab.step] ✅️ expected type: Type, term
          Nat
        [Elab.step.result] Nat
      [Elab.step] ✅️ expected type: Nat, term
          3
        [Elab.step.result] 3
      [Elab.step.result] 3
    [Elab.step] ✅️ expected type: <not-available>, term
        4
      [Elab.step.result] 4
    [Elab.step.result] 3 ≠ 4
  [Elab.step.result] 3 ≠ 4

The symbol ≠ is a macro. Its expansion, binrel% Ne✝ (3 : Nat) 4, hands the two sides to binrel%, an elaborator for binary relations. The dagger after Ne marks a name introduced by the macro, which text written by the user cannot capture; syntax extension and hygienic macros explains this hygiene, which the paper introducing Lean 4 describes as capture-avoiding. The ascription (3 : Nat) passes the expected type Nat down to the numeral 3.

Expected types

The expected type is the elaborator's main source of information. Some notation cannot be read at all without it. The anonymous constructor ⟨1, 2⟩ names no type, so on its own it fails:

#check ⟨1, 2⟩

Lean answers Invalid `⟨...⟩` notation: The expected type of this term could not be determined. With an ascription, #check (⟨1, 2⟩ : Nat × Nat) prints (1, 2) : Nat × Nat: knowing the type, the elaborator finds the structure's one constructor and applies it.

What the elaborator fills in

The option pp.all prints a term with nothing hidden: every implicit argument, every instance, every universe level. It is the way to see what the elaborator actually produced.

#check @id
set_option pp.all true in
#check id 5
set_option pp.all true in
#check (2 : Int) + (3 : Nat)

@id : {α : Sort u_1} → α → α
@id.{1} Nat (@OfNat.ofNat.{0} Nat (nat_lit 5) (instOfNatNat (nat_lit 5))) : Nat
@HAdd.hAdd.{0, 0, 0} Int Int Int (@instHAdd.{0} Int Int.instAdd)
  (@OfNat.ofNat.{0} Int (nat_lit 2) (@instOfNat (nat_lit 2)))
  (@Nat.cast.{0} Int instNatCastInt (@OfNat.ofNat.{0} Nat (nat_lit 3) (instOfNatNat (nat_lit 3)))) : Int

Four kinds of filling are visible.

Implicit arguments. The braces in {α : Sort u_1} mark an argument the user does not write. For id 5 the elaborator creates a placeholder for α, a metavariable, and unifies it with the type of the argument 5, which is itself still open; it becomes Nat when the default instance for numerals is applied, as described under postponement below. Metavariables and unification treats this machinery.

Universe levels. The universe parameter u_1 of id is instantiated to 1, since Nat : Type and Type is Sort 1.

Instances. A numeral is not a primitive: 5 becomes OfNat.ofNat Nat 5 (instOfNatNat 5), and + becomes the method HAdd.hAdd of a type class with the instance instHAdd built on Int.instAdd. The instances are found by search; type classes and instance resolution describes it.

Coercions. The second summand was written as a natural number but is used where an integer is expected. The elaborator inserts Nat.cast, which the ordinary printer shows as ↑. The reference manual states that a coercion is used when a term of one type appears where another is expected, and that coercions are found by type class instance synthesis.

Postponement

The elaborator works through a term roughly from left to right, but information often arrives late. A subterm may need a type that a later argument determines, or an instance problem may still contain unknowns. In such cases the elaborator does not fail. It puts a synthetic metavariable in place of the unfinished work and comes back to it. In Lean 4.34.1 such a placeholder has one of four kinds: an instance to be synthesised, a coercion to be inserted, a tactic block to be run, or a term whose elaboration was postponed.

The pending placeholders are resumed in a fixed order. Lean retries them while progress is being made. When none progresses, it retries without allowing further postponement, then applies default instances to instance problems still unsolved, then forces the remaining problems to succeed or report an error. Tactic blocks run last, when the rest of the term is as complete as it will get.

Default instances explain a small puzzle:

#check fun x => x + 1

Lean prints fun x => x + 1 : Nat → Nat, although nothing in the text says Nat. The type of x is unknown, so the instance problem for + stays stuck through every round. At the default step, Lean's prelude marks instHAdd as a default instance, which makes both summands and the result share one type, and marks instOfNatNat as a low-priority default instance for numerals, which makes that type Nat. Where no default applies, the elaborator reports the gap. Writing def g := fun x => x gives Failed to infer type of binder `x`.

Why the elaborator is not trusted

The elaborator is large, it is written in Lean, and users extend it: every new macro, elaborator or tactic becomes part of it. The design does not ask anyone to trust it. Its output is checked by the Lean kernel, and the reference manual gives the reason: to guard against potential bugs in elaboration. The Lean kernel does no unification of its own and no termination checking; it expects the elaborator to have done that work, and checks the explicit result. As long as its output goes through the Lean kernel, a faulty elaborator can therefore cause a rejection, or a slow check, but not the acceptance of a false theorem. The Lean kernel describes the checker.

One thing the Lean kernel cannot protect is meaning. The elaborator decides what a statement says: which instance + refers to, which coercion was inserted, which type a numeral was given. The Lean kernel then checks a proof of that statement. The reference manual's guidance on validating proofs makes the same separation: where there is doubt that a theorem means what it appears to mean, its statement and every definition it refers to must be examined, particularly where custom notation or type classes are involved. pp.all and #print are the tools for that reading.

Beyond terms

Elaboration also records what it did. Info trees relate the elaborated terms to the user's original syntax, and an editor uses them to show types on hover and goals in a proof. Commands are elaborated too. A command elaborator may add definitions, open namespaces or declare new syntax, and these are changes to Lean's state, not terms. This extensibility, a parser, elaborator and tactic framework that users can extend from Lean itself, is a design aim stated in the abstract and the conclusion of the paper that introduced Lean 4.

Next

The Lean kernel describes what happens to the elaborated term. Metavariables and unification opens up the placeholders used above.