module Nat : sig

      type 'n z
      type 'n s

      type ('a, 'n) nat =
              Zero : ('a, 'n) nat
            | Succ : ('a, 'n) nat -> ('a, 'n s) nat

      val add : ('a, 'n) nat -> ('a, 'n s) nat

      val plus : ('a, 'n) nat -> ('a, 'n) nat -> ('a, 'n) nat

      (*
      val one : ('n s z) nat
      val two : ('n s s z) nat
      val three : ('n s s s z) nat
      val four : ('n s s s s z) nat
      val five : ('n s s s s s z) nat
      val six : ('n s s s s s s z) nat
      val seven : ('n s s s s s s s z) nat
      val eight : ('n s s s s s s s s z) nat
      val nine :  ('n s s s s s s s s s z) nat
      val ten : ('n s s s s s s s s s s z) nat
      *)
end = struct

      type 'n z
      type 'n s

      type ('a, 'n) nat =
              Zero : ('a, 'n) nat
            | Succ : ('a, 'n) nat -> ('a, 'n s) nat

      let add n = Succ n

      let rec plus a b = match a with
            | Succ a -> Succ (plus a b)
            | Zero -> b

      (*
      let one = Succ Zero
      let two = plus one one
      let three = plus two one
      let four = plus two two
      let five = plus three two
      let six = plus three three
      let seven = plus five two
      let eight = plus five three
      let nine = plus five four
      let ten = plus five five
      *)
end