Notation

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.