Skip to main content

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.

Pattern matching is one of Lean 4’s most expressive features. It allows you to inspect the structure of values at the type level, with exhaustiveness checking enforced by the compiler. Pattern matching underpins inductive proofs, recursive functions, and concise data manipulation.

​
Basic match Expressions

A match expression examines a value and dispatches on its constructor: 
def describe (n : Nat) : String :=
  match n with
  | 0 => "zero"
  | 1 => "one"
  | n => s!"some other number: {n}"

#eval describe 0   -- "zero"
#eval describe 1   -- "one"
#eval describe 7   -- "some other number: 7"
You can match on multiple values simultaneously: 
def xor (a b : Bool) : Bool :=
  match a, b with
  | true,  false => true
  | false, true  => true
  | _,     _     => false

​
Wildcard _, Variable, and Constructor Patterns

Pattern formMeaning
_Wildcard — matches anything, binds nothing
xVariable — matches anything, binds to x
Ctor argsConstructor — matches only that constructor
⟨a, b⟩Anonymous constructor
n + 1Successor pattern (for Nat)
-- Wildcard in constructor position
def isNone : Option α → Bool
  | none    => true
  | some _  => false   -- _ ignores the wrapped value

-- Variable pattern captures the matched value
def double : Nat → Nat
  | 0     => 0
  | n + 1 => 2 * n + 2   -- n matches the predecessor

​
Nested Patterns

Patterns can be arbitrarily nested: 
def nested : Option (Option Nat) → String
  | none            => "outer none"
  | some none       => "inner none"
  | some (some 0)   => "double some zero"
  | some (some n)   => s!"double some {n}"

-- Nested tuples
def fst3 : α × β × γ → α
  | (a, _, _) => a

​
Or-Patterns

Multiple patterns can share a single right-hand side using |: 
def isWeekend (day : String) : Bool :=
  match day with
  | "Saturday" | "Sunday" => true
  | _                     => false

inductive Shape where
  | circle  : Float → Shape
  | square  : Float → Shape
  | rect    : Float → Float → Shape

def isRegular : Shape → Bool
  | .circle _ | .square _ => true
  | .rect _ _              => false

​
Guards with if h : ...

A guard condition if h : P then introduces a hypothesis h : P and matches only when the condition holds: 
-- Decision guard on a numeric pattern
def safeSucc (n : Nat) : String :=
  match n with
  | n => if n < 100 then s!"succ = {n + 1}" else "too large"

-- Using if with decidable conditions in match arms (via if h :)
def classify (n : Nat) : String :=
  if h : n < 10 then s!"{n} is small"
  else if h : n < 100 then s!"{n} is medium"
  else s!"{n} is large"
In tactic mode, cases h : e introduces h : e = constructorResult in each branch: 
theorem cases_guard (n : Nat) : n = 0 ∨ n ≥ 1 := by
  cases h : n with
  | zero      => left; rfl
  | succ n    => right; omega

​
Pattern Matching in fun, def, and theorem

Pattern matching is not limited to match — it works directly in function definitions and lambdas: 
-- fun with patterns
def swapPair : α × β → β × α := fun (a, b) => (b, a)

-- Multiple equations in def (equational style)
def fibonacci : Nat → Nat
  | 0 => 0
  | 1 => 1
  | n + 2 => fibonacci n + fibonacci (n + 1)

-- theorem using match
theorem and_left (h : p ∧ q) : p :=
  match h with
  | ⟨hp, _⟩ => hp
Equational-style def foo | pat => ... is syntactic sugar for def foo x := match x with | pat => .... Both compile to the same core term.

​
Exhaustiveness Checking

Lean’s elaborator checks that every possible constructor combination is covered. Omitting a case is a compile error: 
-- This is incomplete and will not compile:
-- def badHead : List α → α
--   | x :: _ => x
-- Error: missing case: []

-- The complete version:
def safeHead? : List α → Option α
  | []     => none
  | x :: _ => some x
If you want to assert a case is unreachable (with a proof), use absurd or nomatch: 
def listLength : List α → Nat
  | []      => 0
  | _ :: xs => 1 + listLength xs

-- nomatch closes a goal when all constructors are covered by hypotheses
example (h : ([] : List Nat) = 1 :: []) : False := by
  simp at h

​
if let and while let

if let matches a single pattern and runs the then-branch only if it matches: 
def doubleIfSome (x : Option Nat) : Option Nat :=
  if let some n := x then some (n * 2) else none

-- In a do block
def printIfSome (x : Option String) : IO Unit := do
  if let some s := x then
    IO.println s!"Got: {s}"
  else
    IO.println "Nothing"
while let repeats as long as the pattern matches (useful with iterators): 
-- Consume elements from a mutable iterator
def sumWhile (arr : Array Nat) : Nat := Id.run do
  let mut total := 0
  let mut i := 0
  while let some n := arr[i]? do
    total := total + n
    i := i + 1
  return total

​
rcases and obtain for Pattern Matching in Tactics

In tactic mode, rcases and obtain provide deep pattern matching on hypotheses: 
-- rcases destructures And, Or, Exists recursively
theorem rcases_example (h : ∃ n : Nat, n > 0 ∧ n < 10) : True := by
  rcases h with ⟨n, hn_pos, hn_lt⟩
  trivial

-- obtain has have-like syntax
theorem obtain_example (h : ∃ n : Nat, n * n = 9) : True := by
  obtain ⟨n, hn⟩ := h
  trivial

-- or-patterns in rcases
theorem or_cases (h : p ∨ q ∨ r) : True := by
  rcases h with hp | hq | hr <;> trivial

​
Structural Recursion: Why It Terminates

Lean 4 requires all functions to terminate. For structurally recursive functions, termination is inferred automatically: each recursive call must be on a sub-term of a constructor argument. 
-- Structurally recursive: each call is on the tail of the list
def myLength : List α → Nat
  | []     => 0
  | _ :: t => 1 + myLength t

-- Structurally recursive on both arguments
def myZip : List α → List β → List (α × β)
  | [],     _      => []
  | _,      []     => []
  | a :: as, b :: bs => (a, b) :: myZip as bs
The termination checker looks for a decreasing measure over the recursive calls. For myLength, each call receives t, which is structurally smaller than _ :: t.

​
Well-Founded Recursion with termination_by

When termination is not immediately obvious from the structure, you provide an explicit measure with termination_by: 
-- Euclidean GCD: terminates because the second argument decreases
def gcd (m n : Nat) : Nat :=
  if n = 0 then m
  else gcd n (m % n)
termination_by n    -- the measure that decreases

-- Ackermann function needs a lexicographic measure
def ackermann : Nat → Nat → Nat
  | 0,     n     => n + 1
  | m + 1, 0     => ackermann m 1
  | m + 1, n + 1 => ackermann m (ackermann (m + 1) n)
termination_by m n => (m, n)    -- lexicographic pair
If you also need to supply a proof that the measure decreases, use decreasing_by: 
-- Array traversal with explicit decreasing proof
def arraySum (arr : Array Nat) (i : Nat := 0) (acc : Nat := 0) : Nat :=
  if h : i < arr.size then
    arraySum arr (i + 1) (acc + arr[i])
  else
    acc
termination_by arr.size - i
decreasing_by exact Nat.sub_succ_lt_self arr.size i h
If termination_by is omitted and Lean cannot infer termination, elaboration fails with a “failed to generate well-founded recursion” error. Always annotate non-structural recursion with termination_by.

​
A Complete Pattern Matching Example

-- A simple expression evaluator using pattern matching throughout
inductive Expr where
  | num  : Int → Expr
  | add  : Expr → Expr → Expr
  | mul  : Expr → Expr → Expr
  | neg  : Expr → Expr
  deriving Repr

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

def simplify : Expr → Expr
  | .add (.num 0) e  => simplify e
  | .add e (.num 0)  => simplify e
  | .mul (.num 1) e  => simplify e
  | .mul (.num 0) _  => .num 0
  | .add e₁ e₂       => .add (simplify e₁) (simplify e₂)
  | .mul e₁ e₂       => .mul (simplify e₁) (simplify e₂)
  | .neg e            => .neg (simplify e)
  | e                 => e

#eval eval (.add (.num 3) (.mul (.num 2) (.num 4)))  -- 11
Pattern matching in Lean 4 is fully supported by the kernel. Each match expression compiles to a sequence of primitive eliminators (recursors) that the kernel can verify. This means exhaustiveness and type-correctness of match arms are enforced at the kernel level, not just by the elaborator.

Build docs developers (and LLMs) love

Get started for freeTalk to us