latte-nats.core
A formalization of the type of natural numbers.
<>
(<> [n nat] [m nat])(not (= n m))
Definition: The inequality on natural numbers.
=
(= [n nat] [m nat])(eq/equality nat n m)
Definition: The equality on natural numbers.
nat
(nat):type
Axiom: The type of natural numbers.
nat-case
(nat-case [P (==> nat :type)])(==> (P zero) (forall [n nat] (P (succ n))) (forall [n nat] (P n)))
Theorem: Case analysis for natural numbers.
nat-induct
(nat-induct [P (==> nat :type)])(==>
(P zero)
(forall [n nat] (==> (P n) (P (succ n))))
(forall [n nat] (P n)))
Axiom: The induction principle for natural numbers.
one
(one)(succ zero)
Definition: The number one.
succ
(succ)(==> nat nat)
Axiom: The successor number.
succ-injective
(succ-injective)(fun/injective succ)
Axiom: The successor function is injective.
succ-single
(succ-single)(forall [n nat] (q/single (lambda [m nat] (= (succ m) n))))
Theorem:
zero
(zero)nat
Axiom: The number zero.
zero-not-succ
(zero-not-succ)(forall [n nat] (<> (succ n) zero))
Axiom: There is not natural number “below” zero.