Module 3 · Lesson 1

Pattern Matching

match takes a value apart by its shape and runs the branch for the case it is in. Most Lean functions over data are written this way.

The Match Expression

Use match to inspect values and branch based on their structure:

lean

Try it

1def describe (n : Nat) : String :=
2  match n with
3  | 0 => "zero"
4  | 1 => "one"
5  | 2 => "two"
6  | _ => "many"  -- underscore matches anything
7
8#eval describe 0  -- "zero"
9#eval describe 5  -- "many"

Each branch has a pattern (left of =>) and a result (right of =>). Lean checks patterns from top to bottom.

Function Definition Syntax

For simple functions, you can pattern match directly in the definition:

lean

Try it

1-- Using match
2def factorial1 (n : Nat) : Nat :=
3  match n with
4  | 0 => 1
5  | n + 1 => (n + 1) * factorial1 n
6
7-- Direct pattern matching (cleaner)
8def factorial2 : Nat → Nat
9  | 0 => 1
10  | n + 1 => (n + 1) * factorial2 n
11
12#eval factorial2 5  -- 120

Key Takeaway

The direct pattern matching syntax (without match) is often cleaner for simple functions. Use match when you need to match in the middle of a larger expression.

Matching on Inductive Types

Pattern matching is the usual way to work with inductive types:

lean

Try it

1inductive Shape where
2  | circle (radius : Float)
3  | rectangle (width : Float) (height : Float)
4  | triangle (base : Float) (height : Float)
5
6def area : Shape → Float
7  | Shape.circle r => 3.14159 * r * r
8  | Shape.rectangle w h => w * h
9  | Shape.triangle b h => 0.5 * b * h
10
11def perimeter : Shape → Float
12  | Shape.circle r => 2.0 * 3.14159 * r
13  | Shape.rectangle w h => 2.0 * (w + h)
14  | Shape.triangle _ _ => 0.0  -- would need side lengths
15
16#eval area (Shape.rectangle 3.0 4.0)  -- 12.000000

Exhaustiveness Checking

Lean refuses to compile if you miss a case:

lean

Try it

1inductive Color where
2  | red | green | blue
3
4-- This won't compile!
5-- def toHex : Color → String
6--   | Color.red => "#FF0000"
7--   | Color.green => "#00FF00"
8--   -- Missing blue case!
9
10-- Complete version:
11def toHex : Color → String
12  | Color.red => "#FF0000"
13  | Color.green => "#00FF00"
14  | Color.blue => "#0000FF"

❗

Lean rejects a match that misses a case, so a forgotten case is a compile error rather than a crash at run time.

Order Matters: First Match Wins

Branches are tried top to bottom, and the first one that matches wins. Lean also tells you when a branch can never be reached:

lean

Try it

1-- Overlapping patterns: (0, 0) matches the first branch, not the second
2def sumPair : Nat × Nat → Nat
3  | (0, b) => b
4  | (a, 0) => a
5  | (a, b) => a + b
6
7#eval sumPair (0, 0)   -- 0, via the FIRST branch
8
9-- Putting the catch-all first makes later branches dead code,
10-- and Lean says so rather than silently ignoring them:
11-- def f : Nat → String
12--   | _ => "catch-all"
13--   | 0 => "zero"
14-- error: Redundant alternative: Any expression matching 0
15--        will match one of the preceding alternatives

💡

Order your branches most-specific first. If you get the redundant alternative error, you have written them backwards — it is a genuine bug report, not a style warning.

Matching Nat: the n + 1 Pattern

Nat looks like a primitive but is an inductive type with constructors zero and succ. The pattern n + 1 is sugar for Nat.succ n:

lean

Try it

1def pred : Nat → Nat
2  | 0     => 0
3  | n + 1 => n
4
5#print pred
6-- fun x => match x with
7--   | 0 => 0
8--   | n.succ => n     ← n + 1 was compiled to Nat.succ n
9
10-- Bigger literal patterns work too, and peel off that many succs
11def describeSmall : Nat → String
12  | 0     => "zero"
13  | 1     => "one"
14  | n + 2 => s!"{n} plus two"
15
16#eval describeSmall 5   -- "3 plus two"

ℹ

The n + 1 spelling is not cosmetic. It is what makes induction and simp line up with your definition later, and it is why the standard library writes xs.length + 1 rather than 1 + xs.length everywhere.

Matching Nothing: nomatch

Some types have no values at all. If you have one in your hands, you are in an impossible situation and can produce anything — nomatchsays exactly that.

lean

Try it

1-- Empty has no constructors, so there is no case to write
2def fromEmpty (x : Empty) : Nat := nomatch x
3
4-- The same trick appears in proofs: from a contradiction, anything follows
5example (h : False) : 2 + 2 = 5 := absurd h (by simp)

Destructuring Structures

Pattern matching works on structures too:

lean

Try it

1structure Point where
2  x : Float
3  y : Float
4
5-- Destructure in the pattern
6def distanceFromOrigin : Point → Float
7  | ⟨x, y⟩ => Float.sqrt (x * x + y * y)
8
9-- Equivalent using field access
10def distanceFromOrigin' (p : Point) : Float :=
11  Float.sqrt (p.x * p.x + p.y * p.y)
12
13#eval distanceFromOrigin ⟨3.0, 4.0⟩  -- 5.000000

Nested Patterns

Patterns can be nested to match complex structures. This helps when one data type sits inside another, such as a list of optional values.

lean

Try it

1-- Match on nested structures
2def firstElement : List (Option Nat) → Option Nat
3  | [] => none
4  | none :: _ => none
5  | some n :: _ => some n
6
7#eval firstElement [some 1, none]  -- some 1
8#eval firstElement [none, some 2]  -- none
9
10-- Match on pairs
11def addPair : Nat × Nat → Nat
12  | (a, b) => a + b
13
14#eval addPair (3, 4)  -- 7

Matching on Multiple Inputs

You can pattern match on multiple arguments at once, which is perfect for combining two values or two lists.

lean

Try it

1def addOptions : Option Nat → Option Nat → Option Nat
2  | some a, some b => some (a + b)
3  | _, _ => none
4
5#eval addOptions (some 2) (some 3)  -- some 5
6#eval addOptions none (some 3)      -- none

Conditions in Branches

Lean does not have Haskell-style pattern guards — there is no | n if n > 0 => …. Instead, match on structure and use if inside the branch:

lean

Try it

1def classifyNumber (n : Int) : String :=
2  match n with
3  | 0 => "zero"
4  | n => if n > 0 then "positive" else "negative"
5
6#eval classifyNumber (-3)   -- "negative"
7
8-- When every case is a condition rather than a shape, skip match entirely
9def grade (score : Nat) : String :=
10  if score >= 90 then "A"
11  else if score >= 80 then "B"
12  else if score >= 70 then "C"
13  else if score >= 60 then "D"
14  else "F"
15
16#eval grade 85  -- "B"

💡

Reach for match when you are asking "what shape is this value?" and for if when you are asking "is this condition true?". A match with a single catch-all pattern and a chain of ifs inside it is always the ifchain written the long way.

Remembering What You Matched: match h : e with

A plain match forgets the connection between the scrutinee and the branch you took. Naming the equation with match h : e with keeps it, which you need once you start proving things about the function.

lean

Try it

1def lookupAt (xs : List Nat) (i : Nat) : String :=
2  match h : xs[i]? with
3  | none   => "out of range"
4  -- inside this branch, h : xs[i]? = some v
5  | some v => s!"found {v}"
6
7#eval lookupAt [1, 2, 3] 1   -- "found 2"

ℹ

Without the h :, once you are inside the some v branch Lean knows v exists but has thrown away the fact that it came from xs[i]?. That fact is exactly what a later proof needs. The cost of writing h : is nothing; the cost of omitting it is sometimes restructuring the whole function.

Or-Patterns

Match multiple patterns with the same result:

lean

Try it

1inductive Weekday where
2  | monday | tuesday | wednesday | thursday | friday | saturday | sunday
3
4def isWeekend : Weekday → Bool
5  | .saturday | .sunday => true
6  | _ => false
7
8-- Without or-patterns (more verbose)
9def isWeekend' : Weekday → Bool
10  | .saturday => true
11  | .sunday => true
12  | _ => false
13
14#eval isWeekend .saturday   -- true

⚠

Every alternative in an or-pattern must bind the same variables with the same types. | .circle r | .rectangle w h => … is rejected, because the two sides disagree about what is in scope. Or-patterns are for cases you treat identically and whose contents you do not need.

As-Patterns

Use @ to bind a name while also destructuring:

lean

Try it

1-- Bind the whole list while also matching head and tail
2def processFirst : List Nat → (Nat × List Nat)
3  | xs@(x :: _) => (x, xs)  -- xs is the whole list, x is the first element
4  | [] => (0, [])
5
6#eval processFirst [1, 2, 3]  -- (1, [1, 2, 3])
7#eval processFirst []         -- (0, [])
8
9-- Useful when you need both the structure and its parts
10def describeOpt : Option Nat → String
11  | opt@(some n) => s!"Value {n}, original: {repr opt}"
12  | none => "None"
13
14#eval describeOpt (some 1)   -- "Value 1, original: some 1"

⚠

Parenthesise the pattern after @ whenever it starts with a bracket. xs@[] does not parse: Lean reads @[ as the start of an attribute and reports a confusing "unexpected token". Write xs@([]), or just match [] directly — there is nothing to name in an empty list.

If-Let and Let-Else

For simple pattern matching with an alternative, use if let:

lean

Try it

1-- if let: match a pattern or take else branch
2def getFirst (xs : List Nat) : Nat :=
3  if let x :: _ := xs then x else 0
4
5#eval getFirst [1, 2, 3]  -- 1
6#eval getFirst []         -- 0
7
8-- Works with any pattern
9def extractValue (opt : Option String) : String :=
10  if let some s := opt then s else "default"
11
12-- let-else: match or diverge early
13def processOption (opt : Option Nat) : IO Nat := do
14  let some n := opt | return 0  -- Early return if none
15  IO.println s!"Processing {n}"
16  return n * 2

💡

Use if let when you have one pattern and a simple fallback. Use match when you have multiple cases or complex logic.

Deep Dive: Pattern Matching Compiles to Efficient Code

Lean compiles a match into nested tests on constructors. Write the clearest match you can; there is no need to reorder branches for speed.

This means you can write clear, declarative patterns without worrying about performance.

Matching on Lists

Lists are commonly pattern-matched to process elements:

lean

Try it

1def sum : List Nat → Nat
2  | [] => 0
3  | x :: xs => x + sum xs
4
5def head? : List α → Option α
6  | [] => none
7  | x :: _ => some x
8
9def tail? : List α → Option (List α)
10  | [] => none
11  | _ :: xs => some xs
12
13def take : Nat → List α → List α
14  | 0, _ => []
15  | _, [] => []
16  | n + 1, x :: xs => x :: take n xs
17
18#eval sum [1, 2, 3, 4, 5]     -- 15
19#eval take 2 [1, 2, 3, 4, 5]  -- [1, 2]

Exercise: Safe Head and Tail

Write a function that returns both the head and tail of a list if it exists.

lean

Try it

1def headTail? : List α → Option (α × List α)
2  | [] => none
3  | x :: xs => some (x, xs)
4
5#eval headTail? [1, 2, 3]  -- some (1, [2, 3])
6#eval headTail? ([] : List Nat)  -- none

Collections & Arrays Next: Recursion