Notation

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

This page fixes the notation used across the edition. The Foundations pages write the rules of Lean's type theory in the notation of the type-theory literature, inside formulas. Lean writes many of the same things in its own syntax, inside code. The tables set the two side by side, with a one-line meaning and the page on which each first appears in the reading order; where the formula and the Lean syntax first appear on different pages, both are named. A dash means that the notation has no counterpart on that side.

The formulas follow Carneiro's presentation of Lean's type theory, as Terms, types and judgments explains; the Lean syntax is that of Lean 4.34.1.

Judgments and rules

A judgment is a statement about the theory, made by its rules; it is not a proposition inside Lean, and Lean has no syntax for asserting one. Lean shows judgments in what it prints: #check prints e : A, and the display of a goal lists a context above ⊢.

in formulas	in Lean	meaning	first used
$\Gamma$	the lines above ⊢ in a goal	a context: variables with their types, $x_1:A_1,\dots ,x_n:A_n$, each type may mention the variables before it	Terms, types and judgments
$⊢$	⊢	in a formula, "derives"; in a goal, it separates what may be used, above, from what must be shown, after it	formula: Terms, types and judgments; goal: Induction, as the machine sees it
$\Gamma ⊢e:A$	e : A, as #check e prints it	the typing judgment: in the context $\Gamma$, the term $e$ has type $A$	Terms, types and judgments
$\Gamma ⊢e\equiv e^{\prime }$	–	definitional equality: $e$ and $e^{\prime }$ are equal by computation and unfolding, with no proof; Lean tests it when it checks rfl	Terms, types and judgments
$e\iff e^{\prime }$	–	Carneiro's algorithmic definitional equality, the relation the Lean kernel's test decides; it implies $e\equiv e^{\prime }$	Definitional equality
$\Gamma \mathrm{o}\mathrm{k}$, $\cdot$	–	the context is well formed; the empty context	Terms, types and judgments
$\frac{J_1{J}_2}{J}$	–	an inference rule: from the judgments above the line, the one below	Terms, types and judgments
$B[a/x]$	–	$B$ with $a$ put in place of the variable $x$	Terms, types and judgments

Functions, types and universes

in formulas	in Lean	meaning	first used
$(x:A)\to B$, $\Pi x:A.B$, $\prod _{a\in A}B(a)$	(x : A) → B, ∀ x : A, B	dependent function type: functions whose result type $B$ may mention the argument $x$; Lean prints it with ∀ when $B$ is a proposition	formula: Terms, types and judgments, $\Pi$ at Dependent function types; Lean: Dependent function types
$A\to B$	A → B	function type, when $B$ does not mention the argument; implication, when $A$ and $B$ are propositions	Propositions as types
$\lambda x:A.e$	fun (x : A) => e, also written fun x ↦ e or λ x => e	function abstraction: the function sending $x$ to $e$	formula: Terms, types and judgments; Lean: What the axioms are
$fa$	f a	application of $f$ to $a$	Terms, types and judgments
$\mathrm{l}\mathrm{e}\mathrm{t}x:A:=v;e$	let x : A := v; e	a local definition	Terms, types and judgments
$\mathrm{S}\mathrm{o}\mathrm{r}\mathrm{t}u$	Sort u	the universe at level $u$, the type of the types at that level	formula: Terms, types and judgments; Lean: Building things from constructors
$\mathrm{S}\mathrm{o}\mathrm{r}\mathrm{t}0$	Prop	the universe of propositions	Propositions as types
$\mathrm{S}\mathrm{o}\mathrm{r}\mathrm{t}(u+1)$	Type u; Type is Type 0	the universes of data	Why there is no type of all types
${\mathrm{U}}_u$	–	Carneiro's name for the universe written $\mathrm{S}\mathrm{o}\mathrm{r}\mathrm{t}u$ in this edition	Terms, types and judgments
$\mathrm{i}\mathrm{m}\mathrm{a}\mathrm{x}uv$	imax u v	the level of a function type: $0$ if $v=0$, otherwise $max(u,v)$	formula: Terms, types and judgments; Lean: Universes and Prop
$c.\{\overline{u}\}$	c.{u}	the constant $c$ used at the universe levels $\overline{u}$	formula: Terms, types and judgments; Lean: Building things from constructors
–	{x : A}, [C A]	an implicit argument, filled in by unification; an instance-implicit argument, filled in by instance resolution	Building things from constructors; explained at Dependent function types
–	⟨a, b⟩	the anonymous constructor: a value of a type with one constructor, such as a pair or a proof of p ∧ q	Propositions as types
–	A × B	the type of pairs	Definitional equality
$\Sigma x:A.B$	(x : A) × B, Σ x : A, B	dependent pair: pairs whose second part has a type that depends on the first	named at Structural and well-founded recursion; no page writes the symbol
$\mathrm{N}\mathrm{a}\mathrm{t}\mathrm{.}\mathrm{r}\mathrm{e}\mathrm{c}$	Nat.rec	the recursor of the natural numbers, at once induction and primitive recursion	formula: Inductive types and recursors; Lean: Building things from constructors
$\prec$, $\mathrm{A}\mathrm{c}\mathrm{c}x$	WellFounded, Acc	a well-founded relation; the proposition that $x$ is accessible, the basis of well-founded recursion	Structural and well-founded recursion

In Lean the dependent function type, function abstraction and the dependent pair are written as in the second column; the reference manual gives the full syntax, including ↦ in place of =>. Each line below is accepted by Lean 4.34.1:

example : Sort 0 = Prop := rfl
example : Sort 1 = Type := rfl
example : Type 1 = Sort 2 := rfl
example : (fun (x : Nat) => x + 1) 2 = 3 := rfl
example : (fun (x : Nat) ↦ x + 1) 2 = 3 := rfl
example : (λ (x : Nat) => x + 1) 2 = 3 := rfl
def pair : (n : Nat) × Fin (n + 1) := ⟨2, 0⟩
def pair' : Σ n : Nat, Fin (n + 1) := ⟨2, 0⟩

#check ∀ x : Nat, x = x
#check (x : Nat) → Fin (x + 1)
#check Nat → Nat
#check fun (x : Nat) => x + 1
#check (Σ n : Nat, Fin (n + 1))

The five #check lines print:

∀ (x : Nat), x = x : Prop
(x : Nat) → Fin (x + 1) : Type
Nat → Nat : Type
fun x => x + 1 : Nat → Nat
(n : Nat) × Fin (n + 1) : Type

The same dependent function type is printed with ∀ when its result is a proposition and with → otherwise, and Lean prints a dependent pair written with Σ in the form (n : Nat) × ….

Logic

in formulas	in Lean	meaning	first used
$\mathrm{\forall }x\varphi$	∀ x : A, P x	for every $x$; a dependent function type into Prop	formula: Classical logic from choice; Lean: Induction, as the machine sees it
$\mathrm{\exists }x\varphi$	∃ x : A, P x, the type Exists	there is an $x$; proved by a witness and a proof, ⟨w, h⟩	formula: Classical logic from choice; Lean: Automation and its limits
–	p ∧ q, the type And	and	Propositions as types
$p\vee q$	p ∨ q, the type Or	or	formula: Classical logic from choice; Lean: Propositions as types
$\mathrm{\neg }p$	¬p, defined as p → False	not	formula: Classical logic from choice; Lean: What the axioms are
$a\leftrightarrow b$	p ↔ q, the type Iff	if and only if	The three axioms
$\mathrm{T}\mathrm{r}\mathrm{u}\mathrm{e}$, $\mathrm{F}\mathrm{a}\mathrm{l}\mathrm{s}\mathrm{e}$	True, False	the proposition with one proof, and the one with none	formula: Classical logic from choice; Lean: True at What the axioms are, False at What has to be trusted
$\ne$	a ≠ b, meaning ¬(a = b)	not equal	formula: Classical logic from choice; Lean: Automation and its limits

Each of these proofs is accepted by Lean 4.34.1; the last shows that ¬p is p → False by definition:

example (p q : Prop) (hp : p) (hq : q) : p ∧ q := ⟨hp, hq⟩
example (p q : Prop) (hp : p) : p ∨ q := Or.inl hp
example (p q : Prop) (h : p → q) (hp : p) : q := h hp
example (p q : Prop) : p ∧ q ↔ q ∧ p := ⟨fun ⟨a, b⟩ => ⟨b, a⟩, fun ⟨a, b⟩ => ⟨b, a⟩⟩
example : ∀ n : Nat, n + 0 = n := fun _ => rfl
example : ∃ n : Nat, n + 2 = 5 := ⟨3, rfl⟩
example : (2 : Nat) ≠ 3 := by decide
example (p : Prop) : (¬p) = (p → False) := rfl

Equality

in formulas	in Lean	meaning	first used
$a=b$	a = b, the type Eq a b	propositional equality: a proposition, whose proofs are terms	formula: Propositional equality; Lean: What the axioms are
$e\equiv e^{\prime }$	–	definitional equality, the judgment above	Terms, types and judgments
$\mathrm{E}\mathrm{q}\mathrm{.}\mathrm{r}\mathrm{e}\mathrm{f}\mathrm{l}a$	rfl, Eq.refl a	the one constructor of equality: a proof of $a=a$	formula: Propositional equality; Lean: Two kinds of equality
$\mathrm{E}\mathrm{q}\mathrm{.}\mathrm{r}\mathrm{e}\mathrm{c}$	Eq.rec	the eliminator of equality: what holds of $a$ holds of $b$ when $a=b$	Propositional equality
–	h ▸ e	substitution: $e$ carried along a proof h : a = b	Propositional equality
–	a ≍ b, the type HEq a b	heterogeneous equality, between terms whose types may differ	Propositional equality
$\mathrm{Q}\mathrm{u}\mathrm{o}\mathrm{t}r$, $\mathrm{Q}\mathrm{u}\mathrm{o}\mathrm{t}\mathrm{.}\mathrm{m}\mathrm{k}ra$	Quot r, Quot.mk r a	the quotient of a type by a relation $r$, and the element of it that $a$ gives	formula: Quotient types; Lean: Propositional equality

example (a b : Nat) (h : a = b) (P : Nat → Prop) (hp : P a) : P b := h ▸ hp
example (n : Nat) (x : Fin n) : x ≍ x := HEq.rfl
#check @HEq

Lean 4.34.1 accepts both and prints @HEq : {α : Sort u_1} → α → {β : Sort u_1} → β → Prop: the two sides of ≍ may have different types.

Holes and unification

in formulas	in Lean	meaning	first used
$?m$	?m.12	a metavariable, a hole the elaborator has yet to fill	formula: Metavariables and unification; Lean: Holes and goals
$s{=}^{?}t$	s =?= t	a unification problem: find values of the metavariables that make the two sides definitionally equal	Metavariables and unification

Metatheory

in formulas	in Lean	meaning	first used
$T⊢\mathrm{C}\mathrm{o}\mathrm{n}(S)$	–	the theory $T$ proves that the theory $S$ is consistent	Consistency and the metatheory
${\mathrm{Z}\mathrm{F}\mathrm{C}}_n$	–	Zermelo–Fraenkel set theory with choice and $n$ inaccessible cardinals	Consistency and the metatheory
${\mathrm{C}\mathrm{I}\mathrm{C}}_n$, ${\mathrm{L}\mathrm{e}\mathrm{a}\mathrm{n}}_n$	–	the Calculus of Inductive Constructions, or Lean's type theory, with $n$ universes	Consistency and the metatheory

Commands and keywords

in Lean	meaning	first used
example : A := e, theorem c : A := e, def c : A := e	a term e of type A, unnamed, as a named theorem, or as a named definition	Propositions as types
by	the term that follows is to be built by tactics	Types as specifications
rfl	the proof of a = a; it closes a goal whose two sides are definitionally equal	Two kinds of equality
sorry	a placeholder for a missing proof, recorded as the axiom sorryAx	What the axioms are
#check e	print the type of e	Why there is no type of all types
#print c	print the definition of c	What the axioms are
#print axioms c	list the axioms that c depends on	What the axioms are
#eval e	compute e and print the result	Functions that always finish

Next

Sources, what was read for the edition.