%% nat.elf - Natural Numbers (Peano Axioms)
%%
%% We define the natural numbers inductively:
%%   - z (zero) is a natural number
%%   - s N (successor of N) is a natural number if N is
%%
%% This gives us: z, s z, s (s z), s (s (s z)), ...
%%              = 0,   1,       2,           3, ...

nat : type.

z : nat.
s : nat -> nat.

%% Equality on natural numbers (identity)
nat-eq : nat -> nat -> type.
nat-eq/refl : nat-eq N N.

%% Inequality (not equal)
nat-neq : nat -> nat -> type.
nat-neq/zs : nat-neq z (s _).
nat-neq/sz : nat-neq (s _) z.
nat-neq/ss : nat-neq (s N) (s M) <- nat-neq N M.

%% Some convenient abbreviations for small numbers
%abbrev one   = s z.
%abbrev two   = s (s z).
%abbrev three = s (s (s z)).
%abbrev four  = s (s (s (s z))).
%abbrev five  = s (s (s (s (s z)))).

%% Predecessor (partial - undefined for zero)
pred : nat -> nat -> type.
pred/s : pred (s N) N.

%% Case analysis principle: every nat is either z or s of something
nat-case : nat -> type.
nat-case/z : nat-case z.
nat-case/s : nat-case (s N).

%% Every natural number has a case
nat-case-total : {N:nat} nat-case N -> type.
%mode nat-case-total +N -C.
nat-case-total/z : nat-case-total z nat-case/z.
nat-case-total/s : nat-case-total (s N) nat-case/s.
%worlds () (nat-case-total _ _).
%total N (nat-case-total N _).