λleanlab

Programs

Factorial

Lean checks that ordinary recursive definitions terminate.

Open Factorial.lean in editor
def factorial : Nat → Nat
  | 0 => 1
  | n + 1 => (n + 1) * factorial n

def main : IO Unit := do
  for n in List.range 8 do
    IO.println s!"{n}! = {factorial n}"

Explanation

| 0 => 1

The base case returns 1 without a recursive call.

n + 1

Matches a successor. The recursive call uses n, which is structurally smaller.

termination

Total recursive functions need a termination argument. Lean can infer it here.

Expected output

Reference only. Run the file to check its actual result.

0! = 1
1! = 1
2! = 2
3! = 6
4! = 24
5! = 120
6! = 720
7! = 5040

Exercise

Compare factorial 10 with factorial 11.