Module 3 · Level 7

Recursion

Recursion is Lean's core looping mechanism. If you can define a function by structural recursion, Lean guarantees it terminates.

Recursive Functions on Nat

lean

1def factorial : Nat → Nat
2  | 0 => 1
3  | n + 1 => (n + 1) * factorial n
4
5#eval factorial 5

Lists are recursive by nature, so many functions mirror the structure of the list.

lean

1def sumList : List Nat → Nat
2  | [] => 0
3  | x :: xs => x + sumList xs
4
5#eval sumList [1, 2, 3]

Exercise: Count Elements

Write a function that returns the length of a list of strings.

lean

1def countStrings : List String → Nat
2  | [] => 0
3  | _ :: xs => 1 + countStrings xs

ℹ

Lean enforces termination. If your recursion is not obviously structural, you will need a termination argument (covered later).

Key Takeaway

Recursion is the idiomatic way to loop in Lean. Structural recursion gives you free termination guarantees.