Module 4 · Level 9 · Premium

Type Classes

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

❗

This is a premium lesson. It adds real-world type class patterns and proof automation workflows.

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.

Premium Track

Premium content includes deeper type class hierarchies and instance search strategies.

View Premium Options

Back: Induction Next: Level 10 · List Proofs (Premium)