Module 4 · Level 9 · Advanced

Type Classes

Type classes let Lean infer behavior automatically. This advanced lesson shows how to define classes, create instances, and build reusable abstractions.

❗

This lesson connects programming abstractions with the instance search machinery used throughout Lean and Mathlib.

Defining a Class

lean

1class Summable (α : Type) where
2  zero : α
3  add : α → α → α
4
5instance : Summable Nat where
6  zero := 0
7  add := Nat.add

Using Instances

lean

1def sumPair [Summable α] (x y : α) : α :=
2  Summable.add x y
3
4#eval sumPair 3 4

Key Takeaway

Type classes encode reusable behavior. They power Lean's numeric operators, ordering, and many proof automation tools.

Advanced Track

The advanced course continues with list proofs, where type class inference and rewriting often appear together.

View Advanced Track

Back: Induction Next: Level 10 · List Proofs