= Solution
Recurse on the first argument for <addition> and <multiplication>, and on the exponent for <exponentiation>:
``
add :: Natural -> Natural -> Natural
add Zero n = n
add (Succ m) n = Succ (add m n)
mul :: Natural -> Natural -> Natural
mul Zero n = Zero
mul (Succ m) n = add n (mul m n)
power :: Natural -> Natural -> Natural
power m Zero = Succ Zero
power m (Succ n) = mul m (power m n)
``
The defining arithmetic identities are
$$
\boxed{0+n=n,\quad(m+1)+n=1+(m+n),\quad0n=0,\quad(m+1)n=n+mn,\quad m^0=1,\quad m^{n+1}=m\,m^n.}
$$
Each recursive call consumes one constructor. The base of <exponentiation> makes `power Zero Zero` equal to one, the empty-product convention. Applying `convert` and using <structural induction> verifies all three operations.
Back to article page
