1.1.1. The natural numbers🔗

Nat is an inductive type: it is generated by a fixed list of constructors (the different possibilities to construct a natural number), the basic ways to build a value. Nat has exactly two (read a : b as a is a term of type b, and a → b as the type of maps from a to b, and succ means the successor of a natural number):

Nat.zero : Nat
Nat.succ : Nat → Nat

so every natural number is a finite tower of them: Nat.zero is 0, Nat.succ Nat.zero is 1, Nat.succ (Nat.succ Nat.zero) is 2, and so on. (The numerals 0, 1, 2 are just notation for these terms.) The general inductive declaration -- how you build your own types this way -- is the subject of a later section; here we only need Nat itself.

Paired with the constructors, and generated automatically alongside the type, is one further tool: the recursor Nat.rec. Where the constructors build a value, the recursor consumes one -- it is the primitive way to define a function with domain Nat. To define some f : Nat → C (where C is some type), you supply exactly two things: a base value base : C for the zero case (i.e. f 0 := base, where f 0 is the Lean way to write f(0)), and a step : Nat → C → C such that, for succ n (which equals n + 1), you may reuse both n and the result already computed for n, i.e. you define in this way f (n + 1) := step n (f n). (Note the important notation here: We write α → β → γ -- with implicit brackets g : α → (β → γ) for a function g mapping every a : α to a function β → γ. So, g a b : γ. In other words, this is the Lean and more flexible way to write a function depending on two variables.)

Noting the example keyword, as well as the inputs C, base, step, we define the terms of type Nat → C by introducing a function (using the fun keyword, and the mapping rule):

Pattern matching, and the cases and induction tactics, which we will encounter in the exercises and below, all compile down to Nat.rec. (The recursor has a still more general form, in which the result type may itself vary with the Nat, and which turns out to unify recursion with the induction principle. That needs the language of universes, so we return to it in the section on inductive types.)

What matters for the next sections is that Nat.rec computes. Applied to a value that is literally one of the two constructors, it selects the matching case -- and the iota rule (ι) made precise below is applied (numerals such as 2 are put into constructor form first, so the rule applies to them too):

Nat.rec base step Nat.zero      ⟶ base
Nat.rec base step (Nat.succ n)  ⟶ step n (Nat.rec base step n)

For a full example, define "double" (note the keyword def at the beginning of the line, and the function name myDouble, the input n : Nat of the function, which returns a Nat) through the recursor and watch it reduce on 2 (here, _ is the name of a variable, which is not used):

The equality myDouble 2 = 4 needs no proof beyond rfl (which is the Lean way of saying that two thing are definitionally equal): both sides reduce to a common form. Naming those reduction steps precisely -- and pinning down when two terms are the same by computation -- is what the rest of this chapter is about.

1.1.2. Definitional equality and rfl🔗

As we just saw, terms in Lean reduce: myDouble 2 reduces to 4. A term reduces, by a fixed set of steps, toward a simpler form -- (fun x => x + 1) 4 becomes 5, and 2 + 2 becomes 4. Each such step is called a reduction and is written term ⟶ simpler term. Two terms are definitionally equal -- also judgmentally equal, written a ≡ b -- when they reduce to a common form, and Lean's kernel then treats them as fully interchangeable, in particular when it compares types during type-checking. That comparison test is called conversion (or defeq checking). Definitional equality must be kept apart from propositional equality a = b, which is itself a Prop and may require a genuine proof; the full three-way distinction -- syntactic, definitional, propositional -- is laid out in the appendix on equality.

The tactic rfl proves exactly a definitional equality. That is why goals whose two sides are written differently but reduce to the same thing close by rfl:

The #eval command (used throughout the chapter on terms) runs the same reduction and prints the resulting value. So rfl, #eval, and every "reduces to" below are one and the same phenomenon. The precise steps are the reduction rules of the kernel, which we now name in full -- they recur throughout the course whenever a later step is claimed to hold "by definition".

1.1.3. Bool🔗

There are inductive types even simpler than Nat. One of them, Bool, is the type with two values, which are called true and false. It has exactly two constructors, neither taking any argument. Here is its definition, straight from Lean's core library (the where keyword introduces the list of constructors):

Bool : Type
Bool : Type

false : Bool

true : Bool

Its recursor Bool.rec consumes a Bool by offering one value for each constructor -- first the false case, then the true case -- and returns the matching one. Into a fixed result C : Type, its (non-dependent) signature is just this, exactly as Nat.rec above:

-- the `false` case first, then the `true` case:
Bool.rec : C → C → Bool → C

This is exactly an if-then-else: reading Bool.rec e f b as "if b then f else e" (note the order: the false result e comes first). Applied to a literal constructor it reduces by the ι rule (the reduction rules below). Equivalently (and definitionally equal) is the following construction (read bif as Boolean if):

Note, as above in the 0 + n = n example, the bif fails to reduce if the value of b is unknown:

The fix is to make a case analysis as follows (cases is a simpler form of induction; see cases and induction):

Note that Bool also carries the usual &&, ||, !.

-- the underlying function, defined by matching on `c`:
def cond {α : Type} (c : Bool) (x y : α) : α :=
  match c with
  | true  => x
  | false => y

-- `bif` is *notation* that expands to a `cond` call:
macro "bif " c:term " then " t:term " else " e:term :
    term => `(cond $c $t $e)

1.1.4. The propositions True and False🔗

Both types in this section live in Prop, the universe of propositions. Before defining them, a word on Prop itself. Unlike Bool, Nat, or the True and False below -- each an inductive type whose definition you can read off -- Prop has no such definition. It is not an inductive type, and there is no def Prop := … to unfold; asking Lean to print it (#print Prop) even fails, because there is nothing written in Lean to print. Instead, Prop is a primitive, baked directly into Lean's kernel: it is the bottom universe Sort 0 (with Type u being Sort (u+1); more on the universe hierarchy in the next chapter). What makes Prop usable is therefore not a definition but the rules the kernel attaches to it -- proof irrelevance and the rest, taken up in why Prop is special.

The trivial proposition True. True is the proposition that always holds. Being a Prop, its terms are proofs. It has a single constructor, taking no argument, which is therefore already a complete proof of it (note that the type after the colon is now Prop, not Type):

True : Prop
True : Prop

intro : True

So proving True is as easy as naming that constructor:

Its recursor has exactly one case, for the single constructor True.intro, so into a fixed result type C its (non-dependent) signature is:

-- one constructor, hence one case:
True.rec : C → True → C

There is correspondingly nothing to learn from a proof of True: the recursor just hands back the value you supplied for that one case (True.rec c h reduces to c), which is why True carries no information.

The empty proposition False. False is the opposite extreme: the proposition that is never true. It is the inductive type with no constructors at all -- so its definition has no where clause and no | lines:

False : Prop
False : Prop

Since there is no constructor, there is no way to build a term of False -- exactly as it should be for a statement that has no proof. Its recursor is the striking one, and here we give its full signature (the result universe Sort u is treated in the next chapter):

False.rec : (motive : False → Sort u) → (t : False) → motive t

-- one constructor → motive implicit, as for `True.rec`
PUnit.rec : {motive …} → motive PUnit.unit →
              (t : PUnit) → motive t
-- no constructor  → motive explicit, as for `False.rec`
Empty.rec : (motive : Empty → Sort u) →
              (t : Empty) → motive t

For ex falso quodlibet, Lean does not use False.rec but False.elim, which is the following:

def False.elim {C : Sort u} (h : False) : C :=
  False.rec (fun _ => C) h

This is exactly what makes False the yardstick of consistency. Because False.elim turns a single proof of False into a proof of every proposition P (the second example above), one term of type False would make every statement a theorem at once -- 0 = 1, its negation, everything -- and the logic would no longer distinguish the provable from the false. A system in which False is inhabited therefore proves nothing of value; it is contradictory. So the entire point of the type theory is arranged around a single requirement: that no term of False can ever be built. Whenever we later call a construction consistent, or note that Lean rejects Type : Type, or that a tactic is sound, it comes back to this -- False must stay empty.

-- We meet False again as the reason a contradiction closes any goal, and all three types return in the discussion of why Prop is special, where False's empty elimination and Bool's two-way split are exactly what mark the line between data and proof.

1.2.1. The universe hierarchy🔗

The answer is a hierarchy: these types-of-types (called universes) are organized into a countably infinite tower, which is exactly what keeps the system consistent.

At the bottom sit the two universes you meet first (Here, the #check command gives the type of a term):

Type (which is the same as Type 0) is the universe of ordinary data types (ℕ, ℝ, Bool, List α, ...), and Prop (which is the universe of propositions, i.e. True/False-statements). But Type cannot contain itself -- that would be paradoxical -- so Type in turn lives in a larger universe Type 1, which lives in Type 2, and so on without end:

1.2.2. How the universe of a type is determined🔗

You rarely write universe levels by hand -- Lean computes the universe of a compound type from the universes of its parts. A function type α → β lands in the larger of the two universes involved:

The same holds for a ∀ (a dependent function type), whose universe is read off from the universe it ranges over together with that of its body. When the body is data -- something in a Type -- the whole ∀ is forced to grow with the domain:

This climbing is what it means for the Type u to be predicative: a predicative definition refers to things already available below it -- whatever a type quantifies over must be strictly smaller, so the type it forms can never land back inside its own domain. That is exactly why ∀ α : Type 5, α → α is pushed up to Type 6, safely above everything it ranges over, and it is what keeps the whole hierarchy well-founded. (The terminology goes back to Poincaré and Russell, who imposed predicativity to outlaw the self-referential definitions behind the set-theoretic paradoxes.)

This is not mere bookkeeping. Suppose ∀ α : Type, α → α were allowed to have type Type rather than Type 1 -- i.e. a ∀ over Type could land back inside Type. That is the first step toward a universe that contains itself, Type : Type, and that is fatal: from Type : Type one can encode Russell's paradox at the level of types -- Girard's paradox -- and derive an honest proof of False, so every proposition becomes provable and the system is worthless. Predicativity, by forcing the climb to Type 1, is exactly what rules this out. (The proof is not short, and Lean's kernel enforces the bump, so you cannot even state ∀ α : Type, α → α : Type to try it; the construction of the paradox from Type : Type is spelled out in the Mathematics part.)

(A definition can also be made to work at any universe level at once; that uses def, so we defer it to the chapter on functions.)

There is exactly one universe that is allowed to break this rule -- Prop -- and that exception is the subject of the next section.

1.2.3. Why Prop is special🔗

Of particular interest is the type Prop, which consists of statements that can be True or False. It includes mathematical statements, so either the hypotheses, or the goal of what is to be proven. A hypothesis in Lean has the form hP : P, which means P is true, and this statement is called hP. Synonomously, it means that P is true and hP is a proof of P. The hypotheses here have names P Q R S, and the proofs of the hypotheses hP hQ hR hS. All names can be arbitrary. Furthermore, there are hypotheses of the form P → Q, which is the statement that P implies Q. (Note the similarity to function notation as in f : ℝ → ℝ.)

We note three specifics which only apply to Prop:

Proof irrelevance: Note that Prop only records that a statement holds, but not which proof we chose. This is proof irrelevance, which means the following goal closes by rfl:

For data living in a Type there is no such collapse, for obvious reasons.

See also Prop vs Type.

Prop is impredicative: Prop is the one universe that escapes the predicativity of the previous section. As long as the body of a ∀ statement is a proposition, the whole ∀ is a Prop -- even when we range over an arbitrarily large universe of types:

Compare this with the Type-valued ∀ α : Type 5, α → α, which had to climb to Type 6. The two statements are syntactically parallel and differ only in their body, yet land in wildly different places -- Prop versus Type 6. A ∀ into Prop stays small; a ∀ into Type u must climb. This is exactly what impredicative means: a proposition may be defined by quantifying over a totality to which it itself belongs. ∀ P : Prop, P is again a Prop, so it ranges over a collection that already contains it -- the definition, so to speak, feeds on itself. Prop is allowed this self-reference because proof irrelevance keeps it harmless.

Restricted (subsingleton) elimination: First, a word on what elimination means. A type's constructors introduce its values -- they are the ways we build them (Or.inl, isTrue, Nat.succ, and so on). Eliminating a value is the opposite: we use it, by looking at which constructor produced it. This is what a match does -- the pattern-matching construct match h with | … => …, taken up properly in the chapter on terms -- and, as we saw in the introduction, it is ultimately the job of the type's recursor. For a proposition P : Prop, then, eliminating a proof means running P's own recursor -- Or.rec, And.rec, and the like (the error below names Or.casesOn, the match-friendly form of Or.rec) -- and the restriction we are about to meet is a restriction on exactly that recursor. To eliminate into a type T means that this case analysis returns a result of type T; eliminating into T, defining a function into T by the recursor, and letting that recursor compute are three names for one act. The restriction on Prop is about exactly this. A proof carries no observable content, so Lean does not let us read data off a proof in this way: otherwise the result could depend on which proof we started from, and proof irrelevance says there is no such difference to observe. So eliminating a proposition may, in general, only produce further propositions, never data. For example, deciding as a Bool which side of a disjunction holds is rejected:

The error message is telling: recursor 'Or.casesOn' can only eliminate into 'Prop'. There is one exception, called subsingleton elimination. If a proposition has at most one constructor and all of its fields are themselves proofs, then it has at most one inhabitant, so eliminating it can reveal nothing -- and Lean does allow it into any type. This covers False (no constructors at all, which is exactly why False.elim closes any goal), Eq (which is why we may rw even in goals that carry data), and And (both of its fields are proofs). It does not cover Or (the disjunction ∨, which has two constructors) or ∃ (its first field is a genuine witness, not a proof). None of this applies to Type: an inductive type in Type always eliminates into anything.

Why must it be this way? This is not red tape -- consistency forces it, and for Or the reason is worth spelling out. What cannot escape here is not a witness (as it would be for ∃) but the tag: the information about which of the two branches holds. Take a true a and consider the proposition a ∨ a. Its two constructors give definitionally equal terms, by proof irrelevance:

Here h : a is a proof of the (true) proposition a. "Left or right?" is simply not a well-posed question about a proof of a ∨ a: the tag is not distinguishable content. So if the rejected (a ∨ b) → Bool above were allowed -- call the resulting function which -- then setting b := a would give which (Or.inl h) = true and which (Or.inr h) = false; but Or.inl h ≡ Or.inr h (they are definitionally equal, the ≡ from the previous chapter), so we would get true ≡ false, a contradiction. Because proofs are indistinguishable, the tag has to stay trapped -- just as a leaked ∃-witness would have forced 3 ≡ 5.

We cannot build such a which -- Lean rejects it -- but we can assume one exists for every a ∨ b (with its left- and right-branch computation rules as hypotheses) and then instantiate at b := a, where the two injections collide. Watch true = false -- hence False -- drop out:

The way out mirrors the one for ∃, one level up. The data-carrying counterpart of a ∨ ¬a is Decidable a (the Decidable typeclass), which -- crucially -- lives in Type, not Prop (its declaration uses the constructor-list where from the Bool section):

Decidable (p : Prop) : Type
Decidable (p : Prop) : Type

isFalse {p : Prop} (h : ¬p) : Decidable p

isTrue {p : Prop} (h : p) : Decidable p

Because Decidable p is in Type, it may eliminate into Type -- which is exactly why if h : p then _ else _ (a dependent if, whose h : p names the proof made available in the then-branch) and the decide tactic compute. The two stories line up exactly:

The classical route mirrors Classical.choose in the same way: Classical.em : a ∨ ¬a is always available (it is a Prop), but its data-carrying counterpart Classical.propDecidable : Decidable a goes through Classical.choice and is therefore noncomputable -- a keyword marking a definition Lean cannot turn into runnable code, needed here because Classical.choice has no computational content to execute (this is the usual trigger for noncomputable, though not the only one). So the two halves -- ∃/Σ/choose for the witness, ∨/Decidable/em for the tag -- are really the same story: computationally relevant information can leave the Prop world only if we put it in Type from the start, or pay for it noncomputably with the axiom of choice. (The Nonempty/Classical.choice form of this is taken up in the chapter on propositions and proofs.)

1.2.4. Inductive types🔗

Many everyday types in Lean -- Nat, List, Option, Bool, even Empty -- are inductive types. We have already dissected two of them, Nat and Bool, in the previous chapter. This section is about the general mechanism -- how you declare such a type yourself, and which declarations Lean accepts.

You declare an inductive type by giving a name, the type's universe, and a list of constructors, each saying how to build a new element out of existing pieces. Declaring the natural numbers by hand reproduces exactly the structure of Nat:

As with Nat, this single declaration introduces three things at once: the type MyNat; its two constructors MyNat.zero and MyNat.succ, so every element is either zero or succ n; and a recursor MyNat.rec -- the type's eliminator, the counterpart of its constructors -- of the same shape as Nat.rec, into which pattern matching, cases, and induction all translate. Its iota rule, MyNat.rec z s (.succ n) ⟶ s n (MyNat.rec z s n), is the firing we watched for Nat. And a recursor is not special to inductive: since a structure is a single-constructor inductive, it too has one -- Point.rec (from the next section) takes a single case, a function of the fields, and the projections Point.x, Point.y are defined through it.

Now that we have universes in hand, we can state the recursor in full generality. The introduction used its non-dependent form, into a fixed result type; the true MyNat.rec lets that type depend on the value being consumed, a dependency recorded by a motive MyNat → Sort u (the leading @ in @MyNat.rec makes Lean's normally-hidden implicit arguments -- here the motive -- explicit, so that #check prints them; see the appendix on parentheses):

With a data-valued motive this is the recursion the introduction showed; with a Prop-valued one it is precisely the induction principle. Recursion and induction are thus two readings of the single primitive MyNat.rec -- which is why the induction tactic and recursive definitions feel so alike.

The declaration only forms the type. How to actually build its elements and define functions on it -- typically by pattern matching on the constructors -- is the subject of the next chapter, on constructing terms.

Proofs about an inductive type use the induction tactic, which applies the recursor for you: one subgoal per constructor, with an induction hypothesis for each recursive argument.

Inductive types also cover non-recursive data:

and parameterized types:

Inductive types are the main mechanism by which new data types enter Lean; Mathlib uses them extensively, and understanding them is essential for reading the library. This also answers the question of the previous section from the other side: the universe of an inductive type must be large enough to hold all of its constructor arguments.

Not every inductive declaration is accepted, though. A constructor may mention the type being defined, but only positively -- never to the left of an arrow inside one of its arguments. This strict positivity condition keeps inductive types built from well-founded data and free of paradox. An infinitely-branching tree -- where a node carries one subtree for each natural number -- is fine, because in the node constructor MyTree occurs only to the right of →:

The leaf case is what gets the type off the ground, and it is worth pausing on why it is needed. Positivity constrains only where MyTree may occur, not whether the type has any elements: drop leaf, and the declaration is still accepted, but no closed MyTree can ever be built -- every node already demands a whole family ℕ → MyTree of subtrees, with nothing to start from, so the type is empty (like Empty; one can even prove MyTree → False). With leaf present you build upward -- leaf 7, then node (fun n => leaf n), then trees over those. Note that leaf here carries a ℕ, so different leaves are genuinely different; a bare leaf : MyTree would give a single, featureless leaf, indistinguishable from every other.

A word on the shape, too. Because node takes a function ℕ → MyTree, every node has one child per natural number -- it branches infinitely. It is not that every MyTree is infinite: a leaf is finite (leaf 7 is a complete tree), so only trees that actually use node are. This infinite branching is inseparable from a function-typed argument; for a finitely-branching tree you would instead write something like node : MyTree → MyTree → MyTree, but there MyTree occurs directly, not inside a function, so the right-of-→ subtlety we are illustrating would not even arise.

But a constructor that stores a function out of the type is rejected:

inductive Bad where
  | mk : (Bad → False) → Bad
-- error: (kernel) arg #1 of 'Bad.mk' has a non positive
--        occurrence of the datatypes being declared

The rejection is not pedantry: were Bad allowed, one could prove False. Project the stored function out of a b : Bad and apply it to b itself,

def app : Bad → (Bad → False) | .mk f => f
def neg (b : Bad) : False := app b b

so neg : Bad → False. Then Bad.mk neg : Bad, and neg (Bad.mk neg) : False is a closed proof of False (it even loops, neg (Bad.mk neg) ⟶ neg (Bad.mk neg) -- the untyped Ω combinator smuggled into the theory). Strict positivity outlaws exactly the negative occurrence that ties this self-applying knot -- the same consistency concern that rules out Type : Type. (That positivity is also sufficient for consistency -- every strictly positive type is the least fixed point of a monotone functor, so the theory has a model -- is a deep metatheorem, not something Lean proves about itself.)

1.2.5. Structures🔗

While inductive types let us define types with multiple constructors, many mathematical objects are better described as a collection of named fields. For example, a point in the plane has an x-coordinate and a y-coordinate. In Lean, we use structure for this.

A structure is a special case of an inductive type with exactly one constructor and named fields. Here is a simple example:

This declares a new type Point whose elements are records with two ℕ fields. (Both must be given in order to define a Point, which is the only way we can make such a Point, i.e. it only has a single constructor.) Like every declaration, it produces more than the type alone: a constructor Point.mk and one projection per field. We can inspect their types without building any value yet:

Fields may be given default values as part of the declaration:

These defaults are used whenever a value is built without specifying every field.

One structure can extend another, inheriting all of its fields:

so a Point3D has fields x, y (from Point) and z. This is particularly important in Mathlib, where the algebraic hierarchy uses structure extension extensively: CommRing extends Ring, which extends Semiring, and so on.

Structures are natural for representing mathematical objects. A Gaussian integer (a complex number with integer parts) is a pair of ℤs,

and a structure may bundle data together with a property -- here a linear map, carrying both a function and a proof that it respects addition (the square brackets [Add α] are an instance-implicit argument, requiring α to carry an addition; see the typeclasses chapter):

This pattern of bundling data with properties is fundamental to how Mathlib organizes mathematics.

How to construct values of these types, read their fields, and define operations on them is the subject of the next chapter.

1.2.6. Inductive types vs structures🔗

When should you use inductive and when structure?

• Use structure when your type has a single constructor with named fields. Examples: points, complex numbers, algebraic structures.

• Use inductive when your type has multiple constructors. Examples: natural numbers, lists, trees, Option, Bool.

A structure is syntactic sugar for an inductive type with one constructor. The definition

structure Point where
  x : ℕ
  y : ℕ

is essentially equivalent to

inductive Point where
  | mk : ℕ → ℕ → Point

but the structure version gives us named fields, dot notation, the possibility for default values, and the extends mechanism. (A class is in turn a structure marked for use by instance search; we return to it in the Typeclass chapter.)

1.2.7. Quotient types🔗

Alongside universes, function types, and inductive types, Lean has one more basic way to form a type: the quotient. Given a type α and a relation r : α → α → Prop, the type Quot r glues together elements that r relates -- it is α "seen up to r". This is how the chapter's opening remark, that ℝ is Cauchy sequences up to an equivalence, becomes an actual construction; ℤ, ℚ, Multiset α (lists up to reordering), and ZMod n are quotients too.

Its entire interface is four constants:

• Quot.mk r sends each element to its class.

• Quot.sound is the crux: if r a b, then the two classes are the same term. It is one of Lean's few genuine axioms -- the #print axioms name command traces a constant back to the axioms it depends on, and here #print axioms Quot.sound reports [Quot.sound].

• Quot.lift defines a function out of the quotient -- but only once you prove it respects r (the ∀ a b, r a b → f a = f b argument), which is exactly the mathematician's "check that this is well-defined". And it computes: Quot.lift f h (Quot.mk r a) reduces to f a.

• Quot.ind proves a property of every quotient element by checking it on the classes Quot.mk r a.

In practice one usually goes through Quotient, a thin wrapper of Quot over a bundled equivalence relation (a Setoid). The status of Quot.sound as an axiom is taken up again in the axioms chapter.

1.3.1. Naming terms with def🔗

The command def gives a name to a term. In its simplest form,

def name : T := term

gives the name name to a term of type T. Using the Point structure from the previous chapter, here are four ways to define a term of type Point:

All four invoke the single constructor of Point: the record form { x := …, y := … }, the anonymous constructor ⟨...⟩ (typed \< and \>), the explicit Point.mk, and the block where form -- one field := value line per field, with no braces or commas. The where form is just the record form spread over several lines; it is the same syntax we will use to supply typeclass instances (instance : Add Vec2 where …), and it has nothing to do with the |-branches of pattern matching (fields are field := value, not | pattern => …).

Here the target type is fixed by the : Point on the left of :=, so Lean knows which constructor { … } and ⟨…⟩ mean. When the type is not clear from the context, you can annotate the record itself:

1.3.2. Constructing and using structure values🔗

We read fields back with dot notation. Here the #eval command evaluates a (computable) term and prints the resulting value -- the same reduction that rfl performs, only with the answer displayed:

We build a new value from an existing one, changing only some fields, with the with keyword:

Since structures are immutable (as everything in functional programming), this creates a new Point rather than modifying p1. You may even draw from several records at once -- { p, q with … } takes each remaining field from the first of p, q that supplies it. When a structure declares field defaults, a value may omit those fields:

For an extended structure we supply all fields, inherited and new:

Operations on a structure are ordinary functions; placing them in the type's namespace lets us call them with dot notation:

p2.normSq (the squared distance from the origin) works because Lean sees that p2 : Point and looks for Point.normSq. The Gaussian-integer type gives a fuller example -- data and its operations together:

1.3.3. Defining and evaluating functions🔗

A function is again just a term -- one whose type is a function type. We define one with def, now writing its arguments before the :=, and evaluate it with #eval. The shape is

def name (arguments) : resultType := body

so the following defines double, taking one argument n : ℕ and returning the ℕ value 2 * n:

Application is written f x (no parentheses -- f x is Lean's way of writing f(x)). A pure function returns the same result for the same arguments, exactly as in mathematics.

Functions of several arguments are curried: a function of two arguments is really a function that takes one argument and returns another function.

The type of add is ℕ → ℕ → ℕ, which reads as ℕ → (ℕ → ℕ); so add 3 is itself a function of type ℕ → ℕ.

1.3.4. Polymorphic functions🔗

Functions can take types as arguments, not just values -- this is how you write a single definition that works for every type. The identity function is the basic example:

Usually you do not want to pass the type explicitly every time, so you make it an implicit argument with braces {...}; Lean then infers it from the value:

A definition that should also work at any universe level -- recall the universe hierarchy -- uses a universe variable. You may introduce one with the universe command, or, most commonly, write Type*, which inserts a fresh universe variable for you:

This is why signatures throughout Mathlib read {α : Type*}: the same definition then applies whether α is small like ℕ or large like Type itself. We use {α : Type*} freely in the examples below.

1.3.5. Anonymous functions🔗

Sometimes we need a quick, throwaway function without giving it a name. We use fun (short for "function") with the ↦ arrow (typed \mapsto):

In mathematics one would write x ↦ x^2; in Lean we write fun x ↦ x ^ 2. There is an even shorter form using the · placeholder (a centered dot, typed \cdot): a · stands for an anonymous argument, so (· + 10) is shorthand for fun x ↦ x + 10, and several · become successive arguments -- (· + ·) means fun x y ↦ x + y.

1.3.6. Pattern matching🔗

For functions on inductive types (like ℕ, List α, Option α, Bool), the most natural way to define them is by pattern matching on the constructors of the input. The syntax uses match ... with and one branch per constructor, each prefixed by a |.

For example, the factorial function on ℕ matches on whether the input is 0 or a successor n + 1:

Each branch may use the variables introduced by its pattern (here n on the right-hand side). Lean checks two things automatically:

1. Exhaustiveness. Every constructor of ℕ is covered (the cases 0 and n + 1 exhaust ℕ). If you forget a case, Lean complains.

2. Termination. The recursive call factorial n is on a strictly smaller argument than n + 1, so the definition is well-founded.

It works just as well for the inductive types you declare yourself. For MyNat from the previous chapter, doubling is defined by matching on the two constructors:

The leading dot in .zero and .succ is anonymous constructor notation: because Lean already knows the result must be a MyNat, we may write .zero in place of the full MyNat.zero. Writing plain zero would fail -- there is no zero in scope, only MyNat.zero.

Pattern matching works for any inductive type:

The same syntax can be used inline with match:

1.3.7. Recursion and termination🔗

The definitions above are recursive: they call themselves on smaller inputs. A classic example with two base cases is the Fibonacci sequence:

Lean only accepts a recursive definition once it is convinced the recursion terminates. For structural recursion -- where each call is on a syntactic sub-part of the input, as in factorial, length', and fib -- this is automatic.

When the recursive call is not on a structural sub-part, you justify termination by giving a measure that strictly decreases: the termination_by clause names the measure, and decreasing_by discharges the proof that it goes down. Euclid's algorithm is the classic example -- euclidGcd m n recurses on n % m, which is not a subterm of m, but the first argument strictly decreases:

Reading it off: termination_by m declares the measure (the first argument); for the recursive call Lean then asks you to show it shrinks, i.e. n % m < m, which is exactly the goal decreasing_by proves (Nat.mod_lt from m ≠ 0; the hypothesis _h is in scope thanks to the dependent if). When the decrease is routine, decreasing_by can often close it with omega:

Under the hood this compiles to well-founded recursion (WellFounded.fix); that theory -- what makes a relation well-founded, and why < on Nat qualifies -- is developed in the Mathematics part.

1.4.1. The problem typeclasses solve🔗

Consider the + operator. It works on natural numbers, integers, real numbers, matrices, polynomials, and many other types. How does Lean know which + to use?

One approach would be to define different functions: addNat, addInt, addReal, etc. But that would be extremely tedious. Instead, Lean uses typeclasses: there is a single Add typeclass, and each type that supports addition provides an instance of Add.

When you write a + b, Lean looks at the types of a and b, finds the appropriate Add instance, and uses it. This process is called instance resolution and happens automatically.

1.4.2. Defining typeclasses🔗

A typeclass is defined using the class keyword. Here is a simplified version of how Add might be defined:

This says: for any type α, an instance of MyAdd α provides a function myAdd : α → α → α. The class keyword is almost the same as structure -- in fact, every class is internally a structure. The difference is operational:

• A structure is constructed and passed explicitly: you write ⟨...⟩ or call its named projections.

• A class is also a structure, but Lean's instance resolution will synthesize one for you whenever a function expects an [Add α] argument. You never write the instance argument by hand.

So the rule of thumb is: use structure when the value is part of the data the user manipulates (a Point, a Person, a RingHom); use class when the value is a canonical piece of structure attached to a type (a Group instance on ℤ, an Add instance on ℕ) and you want Lean to find it automatically.

1.4.3. Data classes and Prop classes🔗

Because a class is a structure, the applied class C α is an ordinary type, and an instance is simply a term of that type. Its universe follows the same rule as any structure -- the largest universe among its fields -- and this splits typeclasses into two kinds.

Data classes bundle operations, so they carry Type-valued fields and live in Type. Their instances are data: a record of operations and proofs, carried at runtime and projected like any structure.

Prop classes have only propositional fields, so they live in Prop, and their instances are proofs. Mathlib's Fact is the standard example -- it merely packages a proof of p as a searchable instance.

Being a proposition, a Prop class inherits proof irrelevance: any two instances are definitionally equal. That is a feature -- such an instance can never conflict with another, and it is erased at runtime.

So typeclasses simply inherit the proof / data split we drew for terms in general: an instance is data or a proof exactly according to whether its class lives in Type or Prop.

It is worth being precise about the role such a term plays. You genuinely do construct it -- that is exactly what instance … where … does, and its fields are ordinary values you can project and run. But you then use it as a property of the type: declared once, synthesized automatically wherever [C α] is required, and essentially never named or passed by hand. For a data class it stays genuine data (carried at runtime); for a Prop class it degenerates to just the fact that it holds -- a proof, erased. So "an instance is only a property, not a term" is right about the usage but not the substance: the term is really there; you simply delegate its construction and handling to instance resolution.

The parallel is exact at the term level, too. Just as class is a structure marked for instance search, instance is a def marked for instance search: instance foo : C := … is sugar for @[instance] def foo : C := …. (A plain def of a class type is a perfectly good term -- only invisible to the search.)

1.4.4. Creating instances🔗

We create instances using the instance keyword:

Now we can use MyAdd.myAdd on natural numbers and integers, and Lean will automatically find the right instance.

Let us define a custom type and give it an Add instance:

We defined two instances: Add Vec2 so we can use +, and ToString Vec2 so Lean can print Vec2 values.

1.4.5. Using deriving🔗

Writing instances by hand is not always necessary: for a range of standard typeclasses Lean can generate the instance automatically, if you append a deriving clause to the type definition.

Without deriving Repr, the #eval command would not know how to print a Student. The deriving clause tells Lean to automatically create a Repr instance. Here is what the commonly derived classes provide:

Several instances can be derived at once:

1.4.6. The square bracket notation🔗

When a function needs a typeclass instance, we use square brackets [...] in its signature:

The [Add α] argument tells Lean: "find an Add instance for α automatically." We do not need to pass it explicitly; Lean's instance resolution handles it.

You can name the instance if you need to refer to it:

But usually the unnamed form [Add α] is preferred, since Lean resolves it behind the scenes.

So [...] is the typeclass bracket: it marks an instance argument, filled by instance search -- as opposed to (...), which you supply yourself, and {...}, which Lean infers by unification. The four kinds of binder brackets (), {}, ⦃⦄, and [] are contrasted side by side in the appendix on parentheses.

1.4.7. Inspecting typeclass arguments with @🔗

When working with Mathlib, it is often useful to see all the implicit and typeclass arguments of a lemma. The @ symbol makes all arguments explicit:

#check mul_comm
-- mul_comm : ∀ {M : Type u_1} [inst : CommMonoid M] (a b : M), a * b = b * a

#check @mul_comm
-- @mul_comm : ∀ {M : Type u_1} → CommMonoid M → M → M → M = M

The first form shows [inst : CommMonoid M] in brackets, meaning it is found automatically. The @ version shows all arguments explicitly, which helps understand exactly what typeclass constraints are required.

1.4.8. The algebraic hierarchy in Mathlib🔗

Mathlib uses typeclasses to build an extensive hierarchy of algebraic structures. Here are some key ones, ordered roughly from weakest to strongest:

• Add α -- a type with an addition operation

• Mul α -- a type with a multiplication operation

• AddMonoid α -- a type with addition, an additive identity 0, and associativity

• Monoid α -- a type with multiplication, a multiplicative identity 1, and associativity

• Group α -- a monoid with inverses

• AddCommGroup α -- a commutative group under addition

• Ring α -- an additive commutative group with a multiplication that distributes over addition

• CommRing α -- a ring with commutative multiplication

• Field α -- a commutative ring where every nonzero element has an inverse

• LinearOrder α -- a type with a total order

Each of these is defined as a class that extends simpler classes. For example (simplified):

class Group (α : Type) extends Monoid α where
  inv : α → α
  inv_mul_cancel : ∀ a : α, inv a * a = 1

When you write a lemma that requires a CommRing, Lean automatically knows that it also has Add, Mul, AddCommGroup, etc., because of the extends chain.

The power of this system is that we can state and prove theorems at the most general level. For instance, mul_comm works for any CommMonoid, which includes ℕ, ℤ, ℚ, ℝ, ℂ, polynomial rings, matrix rings (when the base is commutative), and many more.

1.4.9. Defining multiple instances🔗

Let us build a more complete example. We define a type Mod3 representing integers modulo 3, and equip it with algebraic structure: