Programming · 10 min

Pattern matching and recursion

Pattern matching gives a separate equation for each shape of input. Natural numbers are either zero or a successor, written n + 1. These two cases cover every Nat.

A recursive function calls itself on smaller inputs. Lean checks termination, which matters because definitions also participate in its logic. A base case and a structurally smaller recursive call are enough here.

Exercise

Complete sumTo so sumTo 3 computes 3 + 2 + 1 + 0.

def sumTo : Nat → Nat
  | 0 => 0
  | n + 1 => 0

#eval sumTo 10

def sumTo : Nat → Nat
  | 0 => 0
  | n + 1 => (n + 1) + sumTo n

#eval sumTo 10

Related example