Documentation Index
Fetch the complete documentation index at: https://mintlify.com/leanprover/lean4/llms.txt
Use this file to discover all available pages before exploring further.
Type classes are Lean 4’s mechanism for principled ad-hoc polymorphism. A type class names a collection of operations; an instance proves that a specific type implements those operations; and the elaborator automatically inserts the correct instance at every call site. This page covers declaring classes and instances, the standard library’s key classes, instance synthesis rules, priorities, and how to build class hierarchies with extends.
Declaring a Class
A class declaration introduces a new type class as a special structure. Fields become the methods of the class:
class Describable (α : Type u) where
describe : α → String
class Printable (α : Type u) where
prettyPrint : α → String
lineWidth : Nat := 80 -- field with default value
Describable.describe has type [Describable α] → α → String.
Declaring an Instance
An instance declaration provides a concrete implementation of a class for a specific type:
instance : Describable Nat where
describe n := s!"Nat({n})"
instance : Describable Bool where
describe
| true => "yes"
| false => "no"
-- Use the class method
def showTwo [Describable α] (a b : α) : String :=
describe a ++ " and " ++ describe b
#eval showTwo (3 : Nat) 7 -- "Nat(3) and Nat(7)"
#eval showTwo true false -- "yes and no"
Named Instances
Give an instance a name when you need to refer to it explicitly:
instance instDescribableString : Describable String where
describe s := s!"String(\"{s}\")"
-- Access the instance explicitly
#eval instDescribableString.describe "hello" -- "String(\"hello\")"
Key Standard Library Classes
Arithmetic: Add, Sub, Mul, Div, Neg
Defined in Init.Prelude, these power the +, -, *, /, and - (unary) notations:
class Add (α : Type u) where
add : α → α → α
-- Custom type with Add instance
structure Vec2 where
x : Float
y : Float
deriving Repr
instance : Add Vec2 where
add a b := { x := a.x + b.x, y := a.y + b.y }
#eval ({ x := 1.0, y := 2.0 } : Vec2) + { x := 3.0, y := 4.0 }
-- { x := 4.0, y := 6.0 }
Repr — Pretty Printing
Repr α provides the repr function used by #eval to display values:
inductive Color where | red | green | blue
deriving Repr -- auto-derived
-- Or manual:
instance : Repr Color where
reprPrec c _ :=
match c with
| .red => "Color.red"
| .green => "Color.green"
| .blue => "Color.blue"
#eval Color.green -- Color.green
ToString
ToString provides toString, used in string interpolation s!"…{x}…":
instance : ToString Color where
toString
| .red => "red"
| .green => "green"
| .blue => "blue"
#eval s!"My favorite color is {Color.blue}"
-- "My favorite color is blue"
BEq — Boolean Equality
class BEq (α : Type u) where
beq : α → α → Bool
-- Provides the == operator
instance : BEq Color where
beq a b :=
match a, b with
| .red, .red => true
| .green, .green => true
| .blue, .blue => true
| _, _ => false
#eval Color.red == Color.red -- true
#eval Color.red == Color.blue -- false
Ord — Three-Way Comparison
class Ord (α : Type u) where
compare : α → α → Ordering
-- Ordering is: .lt | .eq | .gt
instance : Ord Color where
compare a b :=
match a, b with
| .red, .red => .eq
| .red, _ => .lt
| .green, .red => .gt
| .green, .green => .eq
| .green, .blue => .lt
| .blue, .blue => .eq
| .blue, _ => .gt
#eval compare Color.red Color.blue -- Ordering.lt
Inhabited — Default Values
class Inhabited (α : Sort u) where
default : α
-- Every Nat has default 0
#eval (default : Nat) -- 0
-- Every String has default ""
#eval (default : String) -- ""
-- Your own type
instance : Inhabited Color where
default := .red
#eval (default : Color) -- Color.red
Functor and Monad
Functor and Monad enable map and do-notation respectively:
-- Functor: map a function over a container
#eval [1, 2, 3].map (· * 10) -- [10, 20, 30]
#eval (some 5).map (· + 1) -- some 6
#eval (none : Option Nat).map (· + 1) -- none
-- Monad: sequential composition with >>= and do-notation
def safeDivide (n d : Nat) : Option Nat :=
if d == 0 then none else some (n / d)
def computation : Option Nat := do
let a ← safeDivide 100 5 -- some 20
let b ← safeDivide a 4 -- some 5
return b + 1 -- some 6
#eval computation -- some 6
Instance Synthesis
When Lean needs to fill in an instance argument [C α], it searches the instance database for declarations matching the goal type. The search is depth-first and can combine instances:
-- Lean automatically combines these instances:
instance instBEqList [BEq α] : BEq (List α) where
beq xs ys :=
xs.length == ys.length &&
(xs.zip ys).all (fun (a, b) => a == b)
-- Works because [BEq Nat] already exists
#eval ([1, 2, 3] : List Nat) == [1, 2, 3] -- true
#eval ([1, 2, 3] : List Nat) == [1, 2, 4] -- false
Priorities
When multiple instances could satisfy the same goal, Lean uses priority to pick one. Higher numbers win. The default priority is 1000:
instance (priority := 2000) highPriorityInst : BEq MyType where
beq _ _ := true -- always equal (silly example)
instance (priority := 100) lowPriorityInst : BEq MyType where
beq a b := a.field == b.field
-- highPriorityInst is chosen because 2000 > 100
| Keyword | Value |
|---|
high | 1100 |
default | 1000 |
mid | 500 |
low | 100 |
instance (priority := low) : Repr MyType where
reprPrec _ _ := "..."
Default Instances
A @[default_instance] is selected even when the type is not yet fully known. Lean uses this to pick Nat as the default numeric type:
@[default_instance 100]
instance instOfNatNat (n : Nat) : OfNat Nat n where
ofNat := n
-- So `#eval 42` infers 42 : Nat rather than requiring an annotation
@[default_instance]
instance : Inhabited MyConfig where
default := { host := "localhost", port := 8080 }
Class Hierarchies with extends
extends creates a subclass that inherits all parent methods and adds its own:
class Eq' (α : Type u) where
eq : α → α → Bool
class Ord' (α : Type u) extends Eq' α where
compare : α → α → Ordering
-- We can provide a default implementation in terms of compare
eq a b :=
match compare a b with
| .eq => true
| _ => false
Ord' automatically provides an instance of Eq':
instance : Ord' Nat where
compare a b :=
if a < b then .lt
else if a > b then .gt
else .eq
-- This also works because Ord' extends Eq':
#eval Eq'.eq (3 : Nat) 3 -- true
Multiple Inheritance
A class can extend multiple parents:
class Printable' (α : Type u) extends Repr α, ToString α
-- An instance of Printable' must implement both Repr and ToString methods
outParam for Functional Dependencies
Use outParam to indicate that a class parameter is determined by the other parameters. This controls the order in which Lean solves instance goals:
-- HAdd: the output type γ is determined by α and β
class HAdd (α : Type u) (β : Type v) (γ : outParam (Type w)) where
hAdd : α → β → γ
-- This allows Lean to infer γ once α and β are known:
#check (1 : Nat) + (2 : Nat) -- Nat (γ is inferred as Nat)
@[simp] on Instance Lemmas
You can mark theorems about class operations with @[simp] to automate proofs:
@[simp]
theorem beq_self_eq_true [BEq α] [ReflBEq α] (a : α) : (a == a) = true :=
BEq.rfl
-- simp now closes goals involving a == a automatically
example (n : Nat) : (n == n) = true := by simp
Inspecting Instances
Use #check and #print to explore the class hierarchy:
#check @Functor.map
-- Functor.map : {f : Type u_1 → Type u_2} → [inst : Functor f] → (α → β) → f α → f β
#print Monad
-- class Monad (m : Type u_1 → Type u_2) extends Applicative m ...
-- Inspect a specific instance
#check @instBEqList
When writing polymorphic functions, prefer typeclass constraints like [BEq α] over concrete types. This keeps your code reusable and enables the synthesizer to pick the right implementation automatically.
