nat : type.
z : nat.
succ : nat → nat.

rec add : ( ⊢ nat) → ( ⊢ nat) → ( ⊢ nat) =
fn x ⇒ fn y ⇒
  case x of
  | [ ⊢ z] ⇒ y
  | [ ⊢ succ N] ⇒ let [ ⊢ R] = add [ ⊢ N] y in [ ⊢ succ R];

© Computation and Logic Group McGill University Logo
Department of Computer Science, McGill University
3480 University Street, Montreal, Quebec, Canada, H3A 0E9