[3 / 0 / ?]
Quoted By:
You have a basic type of natural numbers.
You can pattern match on them.
That pattern ensures that the parameter is >= 3.
You have syntactic sugar for natural numbers.
How would you write
Thus n+k is just pattern matching on pure naturals, proving that n+k is not harmful.
data Nat = Zero | Succ NatYou can pattern match on them.
f (Succ (Succ (Succ n))) = n `times` (Succ (Succ (Succ Zero)))That pattern ensures that the parameter is >= 3.
You have syntactic sugar for natural numbers.
data Nat = 0 | 1 | 2 | ...How would you write
f more simply?f (n+3) = n * 3Thus n+k is just pattern matching on pure naturals, proving that n+k is not harmful.
