[PostScript]
IntegerAndNatural (Int, N): trait
  % Conversions between Int's and N's
  includes
    Integer (Int),
    Natural (N)
  introduces
    int: N -> Int
    nat: Int -> N
  asserts forall n: N
    int(0) == 0;
    int(succ(n)) == succ(int(n));
    nat(int(n)) == n
[Table of Contents] [Index]