Module 2 · Level 6

Pattern Matching

Pattern matching is the cleanest way to deconstruct data and express branching logic in Lean. It is essential for recursion and proofs.

Matching on Nat

lean

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

Matching on Option

Option types require you to handle some and none.

lean

1def showOption (value : Option String) : String :=
2  match value with
3  | some name => s!"Hello {name}"
4  | none => "No name"
5
6#eval showOption (some "Lean")
7#eval showOption none

Exercise: Match on Lists

Write a function that returns the first element of a list or noneif the list is empty.

lean

1def headOption (xs : List Nat) : Option Nat :=
2  match xs with
3  | [] => none
4  | x :: _ => some x

💡

Pattern matching keeps your code total: you must cover every case.

Key Takeaway

Pattern matching is Lean's go-to tool for branching logic and data deconstruction.

Back: Logic Gates Next: Level 7 · Recursion