## Exercise 3.20
(a) Define
subN ∷ Nat → Nat → Maybe Nat
as a foldN instance.
Our recursive definition of the function is
subN Zero Zero = Just Zero
subN (Succ m) Zero = Just (Succ m)
subN Zero (Succ n) = Nothing
subN (Succ m) (Succ n) = subN m n
We′ve written disjoint cases, but the first two could be unified if we
assume sequential testing.
We have
subN m = foldN (Just m) pred
where
pred Nothing = Nothing
pred (Just n) = predN n
TODO: derive this or prove that it holds.
(b) Define eqN ∷ Nat → Nat → Bool
eqN m n = case subN m n of
Just Zero -> True
Just (Succ x) -> False
(c) Define lessN ∷ Nat → Nat → Bool
lessN m n = case subN m n of
Nothing -> True
Just _ -> False