%% Examples from Lecture Notes %% Section 3.5 Primitive Recursion val pred : nat -> nat = fn x => rec x of p 0 => 0 | p (s x') => x' end; val double : nat -> nat = fn x => rec x of d 0 => 0 | d (s x') => s (s (d x')) end; val plus : nat -> nat -> nat = fn x => fn y => rec x of p 0 => y | p (s x') => s (p x') end; val times : nat -> nat -> nat = fn x => fn y => rec x of t 0 => (s 0) | t (s x') => plus y (t x') end; val half12 : nat -> (nat * nat) = fn x => rec x of h 0 => (0, 0) | h (s x') => (snd (h x'), s (fst (h x'))) end; val half : nat -> nat = fn x => fst (half12 x); val minus : nat -> nat -> nat = fn x => rec x of m 0 => fn y => 0 | m (s x') => fn y => rec y of p 0 => (s x') | p (s y') => m x' y' end end;