Inductive Types and Pattern Matching in Lean 4

Inductive types are the backbone of data representation in Lean 4. From a simple Bool with two constructors to a dependent vector indexed by its length, all data types in Lean 4 are either built-in primitives or defined with the inductive keyword. This page explains the full spectrum of inductive definitions, pattern matching, structures, and the deriving clause.

Simple Enumerations

An inductive type with only nullary constructors is a plain enumeration:

inductive Direction where
  | north : Direction
  | south : Direction
  | east  : Direction
  | west  : Direction

def opposite : Direction → Direction
  | .north => .south
  | .south => .north
  | .east  => .west
  | .west  => .east

#eval opposite .north   -- Direction.south

Inside a match or function definition, you can use the anonymous constructor syntax .north (with a leading dot) when Lean can infer the type.

Recursive Types

An inductive type can refer to itself in its constructors:

`Nat` — Natural Numbers

Nat is defined in Init.Prelude as:

inductive Nat where
  | zero : Nat
  | succ (n : Nat) : Nat

The compiler replaces this with an efficient GMP-backed implementation, but the logical definition is exactly this two-constructor type.

Custom Linked List

inductive MyList (α : Type u) where
  | nil  : MyList α
  | cons : α → MyList α → MyList α

def MyList.length : MyList α → Nat
  | .nil        => 0
  | .cons _ xs  => 1 + xs.length

def MyList.map (f : α → β) : MyList α → MyList β
  | .nil        => .nil
  | .cons x xs  => .cons (f x) (xs.map f)

#eval (MyList.cons 1 (MyList.cons 2 MyList.nil)).length  -- 2

Binary Tree

inductive Tree (α : Type u) where
  | leaf : Tree α
  | node : Tree α → α → Tree α → Tree α

def Tree.size : Tree α → Nat
  | .leaf         => 0
  | .node l _ r  => 1 + l.size + r.size

def Tree.insert [Ord α] (x : α) : Tree α → Tree α
  | .leaf => .node .leaf x .leaf
  | .node l v r =>
    match compare x v with
    | .lt => .node (l.insert x) v r
    | .eq => .node l v r
    | .gt => .node l v (r.insert x)

Parameterized Types

Types can have type parameters:

inductive Either (α β : Type u) where
  | left  : α → Either α β
  | right : β → Either α β

def Either.mapRight (f : β → γ) : Either α β → Either α γ
  | .left a  => .left a
  | .right b => .right (f b)

`structure` — Single-Constructor Inductives

structure is syntactic sugar for an inductive with exactly one constructor. It automatically generates projection functions for each field:

structure Point where
  x : Float
  y : Float

-- Generated: Point.x : Point → Float, Point.y : Point → Float
-- and constructor: Point.mk : Float → Float → Point

def origin : Point := { x := 0.0, y := 0.0 }
def moveRight (p : Point) (dx : Float) : Point := { p with x := p.x + dx }

#eval origin.x      -- 0.0
#eval (moveRight origin 3.0).x  -- 3.0

Structures support inheritance via extends:

structure Point3D extends Point where
  z : Float

def pt3 : Point3D := { x := 1.0, y := 2.0, z := 3.0 }
#eval pt3.x    -- 1.0  (inherited field)
#eval pt3.z    -- 3.0

Dependent Inductive Types (Indexed Families)

The most powerful form: the return type of each constructor can mention the index values. This encodes invariants in the type itself.

`Vector` — Length-Indexed Lists

inductive Vector (α : Type u) : Nat → Type u where
  | nil  : Vector α 0
  | cons : α → Vector α n → Vector α (n + 1)

-- The type system tracks the length
def Vector.head : Vector α (n + 1) → α
  | .cons x _ => x

def Vector.zip : Vector α n → Vector β n → Vector (α × β) n
  | .nil,       .nil       => .nil
  | .cons a as, .cons b bs => .cons (a, b) (zip as bs)

-- Length-3 vector
def v : Vector Nat 3 := .cons 1 (.cons 2 (.cons 3 .nil))
#eval v.head    -- 1

`Fin` — Bounded Natural Numbers

Fin n is the type of natural numbers strictly less than n:

-- Fin is defined as:
-- structure Fin (n : Nat) where
--   val  : Nat
--   isLt : val < n

def lastIndex (n : Nat) (h : 0 < n) : Fin n := ⟨n - 1, Nat.sub_lt h (by omega)⟩

The Recursor

Every inductive type automatically generates a recursor (also called the elimination principle). For Nat, the recursor is:

-- Nat.rec (generated automatically):
-- Nat.rec : {motive : Nat → Sort u}
--         → motive 0
--         → ((n : Nat) → motive n → motive (n + 1))
--         → (n : Nat) → motive n

You rarely use the recursor directly — match expressions and tactics like induction compile down to it. But it is the foundational principle that makes induction work:

-- Proof by induction using the recursor explicitly
theorem zero_add_explicit (n : Nat) : 0 + n = n :=
  Nat.rec
    (motive := fun n => 0 + n = n)
    rfl                              -- base case: 0 + 0 = 0
    (fun n ih => by simp [Nat.add_succ, ih])  -- step case

Pattern Matching

Pattern matching is the standard way to deconstruct inductive values:

inductive Expr where
  | num  : Int    → Expr
  | add  : Expr   → Expr → Expr
  | mul  : Expr   → Expr → Expr
  | neg  : Expr   → Expr

def Expr.eval : Expr → Int
  | .num n     => n
  | .add e1 e2 => eval e1 + eval e2
  | .mul e1 e2 => eval e1 * eval e2
  | .neg e     => -eval e

-- Nested patterns
def Expr.simplify : Expr → Expr
  | .add (.num 0) e     => simplify e          -- 0 + e → e
  | .add e (.num 0)     => simplify e          -- e + 0 → e
  | .mul (.num 0) _     => .num 0              -- 0 * e → 0
  | .mul (.num 1) e     => simplify e          -- 1 * e → e
  | .add e1 e2          => .add (simplify e1) (simplify e2)
  | .mul e1 e2          => .mul (simplify e1) (simplify e2)
  | .neg e              => .neg (simplify e)
  | e                   => e

Guards in Patterns

def classify (n : Int) : String :=
  match n with
  | n if n < 0  => "negative"
  | 0           => "zero"
  | n if n > 0  => "positive"
  | _           => "unreachable"

The `deriving` Clause

deriving automatically generates typeclass instances for an inductive type:

inductive Color where
  | red
  | green
  | blue
  deriving Repr, BEq, Inhabited, DecidableEq, Ord, Hashable

-- Repr: pretty-print with #eval
#eval Color.red      -- Color.red

-- BEq: == operator
#eval Color.red == Color.blue   -- false

-- Inhabited: provides a default value
#eval (default : Color)   -- Color.red (first constructor)

-- DecidableEq: decidable equality, enables `if c1 = c2 then ...`
#eval if Color.green = Color.green then "same" else "different"  -- "same"

Common `deriving` Targets

Class	Effect
`Repr`	Generates `#eval` display and `repr` function
`BEq`	Generates `==` Boolean equality
`Inhabited`	Provides `default` (uses the first constructor)
`DecidableEq`	Makes equality decidable (`if a = b then …`)
`Ord`	Generates `compare : α → α → Ordering`
`Hashable`	Generates `hash : α → UInt64`
`ToString`	Generates `toString` for string interpolation

Deriving for Structures

structure Config where
  host    : String := "localhost"
  port    : Nat    := 8080
  debug   : Bool   := false
  deriving Repr, BEq

def defaultConfig : Config := {}
#eval defaultConfig
-- { host := "localhost", port := 8080, debug := false }

Mutual Inductive Types

mutual
  inductive Even where
    | zero  : Even
    | succOdd : Odd → Even

  inductive Odd where
    | succEven : Even → Odd
end

def Even.toNat : Even → Nat
  | .zero       => 0
  | .succOdd o  => o.toNat + 1

def Odd.toNat : Odd → Nat
  | .succEven e => e.toNat + 1

`class` as Inductive Sugar

class is syntactic sugar for structure with special instance synthesis behaviour (see Type Classes):

class Printable (α : Type u) where
  print : α → String

instance : Printable Nat where
  print n := s!"Nat({n})"

Introduction

Language Basics

Theorem Proving

Functional Programming

Inductive Types and Pattern Matching in Lean 4

Simple Enumerations

Recursive Types

`Nat` — Natural Numbers

Custom Linked List

Binary Tree

Parameterized Types

`structure` — Single-Constructor Inductives

Dependent Inductive Types (Indexed Families)

`Vector` — Length-Indexed Lists

`Fin` — Bounded Natural Numbers

The Recursor

Pattern Matching

Guards in Patterns

The `deriving` Clause

Common `deriving` Targets

Deriving for Structures

Mutual Inductive Types

`class` as Inductive Sugar

Build docs developers (and LLMs) love

Introduction

Language Basics

Theorem Proving

Functional Programming

Documentation Index

​Simple Enumerations

​Recursive Types

​Nat — Natural Numbers

​Custom Linked List

​Binary Tree

​Parameterized Types

​structure — Single-Constructor Inductives

​Dependent Inductive Types (Indexed Families)

​Vector — Length-Indexed Lists

​Fin — Bounded Natural Numbers

​The Recursor

​Pattern Matching

​Guards in Patterns

​The deriving Clause

​Common deriving Targets

​Deriving for Structures

​Mutual Inductive Types

​class as Inductive Sugar

Build docs developers (and LLMs) love

Simple Enumerations

Recursive Types

`Nat` — Natural Numbers

Custom Linked List

Binary Tree

Parameterized Types

`structure` — Single-Constructor Inductives

Dependent Inductive Types (Indexed Families)

`Vector` — Length-Indexed Lists

`Fin` — Bounded Natural Numbers

The Recursor

Pattern Matching

Guards in Patterns

The `deriving` Clause

Common `deriving` Targets

Deriving for Structures

Mutual Inductive Types

`class` as Inductive Sugar