Match Examples

To see how match works, we consider an example with Nat, which is a non-trivial inductive type. We will see how to define functions by recursion on Nat.

def Nat.double (n : ℕ) : ℕ

Equations

• Nat.double 0 = 0
• m.succ.double = m.double.succ.succ

Double of a natural number defined in a more complicated way.

def Nat.double' (n : ℕ) : ℕ

Equations

• Nat.double' 0 = 0
• Nat.double' 1 = 2
• Nat.double' 7 = 14
• m.succ.succ.succ.double' = m.double' + 6
• m.succ.double' = m.double' + 2

A non-terminating function defined using match.

partial def Nat.notDouble (n : ℕ) : ℕ