The Ackermann function is a classic example of a function that is not primitive recursive. It grows very quickly. But Lean's termination checker sees that it is terminating.

@[irreducible]

def ackermann : Nat → Nat → Nat

The Ackermann function is defined by recursion on two natural numbers. It grows very quickly.

Equations

• ackermann 0 x✝ = x✝ + 1
• ackermann m.succ 0 = ackermann m 1
• ackermann m.succ n.succ = ackermann m (ackermann (m + 1) n)