Latte-nats 0.7.0-SNAPSHOT
Released under the MIT Licence
A formalization of natural numbers in LaTTe.
Installation
To install, add the following dependency to your project or build file:
[latte-nats "0.7.0-SNAPSHOT"]
Namespaces
latte-nats.plus
The addition defined on ℕ.
Public variables and functions:
- +
- add-prop
- add-unique
- associative-plus
- cancel-left-plus
- cancel-right-plus
- commutative-plus
- identity-left-plus
- identity-plus
- identity-right-plus
- monoid-plus
- plus
- plus-any-zero-left
- plus-any-zero-right
- plus-assoc
- plus-comm-assoc
- plus-commute
- plus-left-cancel
- plus-left-cancel-conv
- plus-prop
- plus-refl-zero
- plus-right-cancel
- plus-right-cancel-conv
- plus-succ
- plus-succ-swap
- plus-succ-sym
- plus-zero
- plus-zero-swap
- unique-identity-plus
latte-nats.rec
The recursion theorem for natural numbers, together with its complete (somewhat non-trivial) formal proof.
Public variables and functions:
- nat-fixpoint-elem
- nat-fixpoint-fun
- nat-fixpoint-fun-prop
- nat-fixpoint-functional
- nat-fixpoint-prop
- nat-fixpoint-rel
- nat-fixpoint-rel-ex
- nat-fixpoint-rel-sing
- nat-fixpoint-rel-sing-succ-aux
- nat-fixpoint-rel-sing-zero-aux
- nat-fixpoint-rel-uniq
- nat-fixpoint-succ
- nat-fixpoint-zero
- nat-rec-ex
- nat-rec-single
- nat-recur
- nat-recur-prop
- nat-recur-prop-prop-rel
- nat-recur-prop-rel
- nat-recur-prop-rel-prop
- nat-recur-rel-prop-rel-prop