Latte-integers 0.12.0-SNAPSHOT
Released under the MIT Licence
A formalization of integers in LaTTe.
Installation
To install, add the following dependency to your project or build file:
[latte-integers "0.12.0-SNAPSHOT"]
Namespaces
latte-integers.minus
The subtraction (and opposite) defined on ℤ.
Public variables and functions:
- -
- --
- assoc-minus-minus
- assoc-minus-minus-sym
- assoc-minus-plus
- assoc-minus-plus-sym
- assoc-plus-minus
- assoc-plus-minus-sym
- minus-cancel
- minus-left-cancel
- minus-one
- minus-opp
- minus-opp-cancel
- minus-pos-neg
- minus-pos-neg-conv
- minus-pos-neg-equiv
- minus-pred
- minus-pred-succ
- minus-pred-succ-sym
- minus-prop
- minus-prop-cons
- minus-right-cancel
- minus-succ
- minus-succ-pred
- minus-succ-pred-sym
- minus-unique
- minus-zero
- minus-zero-alt
- minus-zero-alt-conv
- nat-split-opp
- opp-and-zero
- opp-eq
- opp-nat-split
- opp-nat-split-conv
- opp-nat-split-equiv
- opp-neg-pos
- opp-neg-pos-conv
- opp-neg-pos-equiv
- opp-neg-split
- opp-opp
- opp-plus
- opp-plus-opp
- opp-pos-neg
- opp-pos-neg-conv
- opp-pos-neg-equiv
- opp-pos-split
- opp-pred-succ
- opp-succ-pred
- opp-zero
- plus-opp-minus
- plus-zero-minus
- zero-opp-zero
- zero-opp-zero-conv
- zero-opp-zero-equiv
latte-integers.nat
The natural integers in ℕ as a subset of ℤ.
Public variables and functions:
- int-split
- int-split-alt
- int-split-elim
- int-split-elim-rule
- int-split-zero
- nat
- nat-case
- nat-induct
- nat-split
- nat-succ
- nat-succ-injective
- nat-succ-prop
- nat-zero
- nat-zero-has-no-pred
- nat-zero-is-not-succ
- negative
- negative-nat
- negative-not-zero
- negative-pred
- negative-pred-split
- negative-pred-split-conv
- negative-pred-split-equiv
- negative-pred-zero
- positive
- positive-conv
- positive-nat-split
- positive-not-zero
- positive-succ
- positive-succ-conv
- positive-succ-equiv
- positive-succ-split
- positive-succ-split-conv
- positive-succ-split-equiv
- positive-succ-strong
- positive-zero-conv
- zero-is-not-one
latte-integers.ord
The natural ordering on integers.
Public variables and functions:
- <
- <=
- >
- >=
- le-antisym
- le-lt-split
- le-refl
- le-trans
- lt-asym
- lt-le
- lt-opp
- lt-opp-conv
- lt-opp-equiv
- lt-pred
- lt-pred-cong
- lt-pred-cong-conv
- lt-succ
- lt-succ-cong
- lt-succ-cong-conv
- lt-succ-weak
- lt-trans
- lt-trans-weak
- lt-trans-weak-alt
- lt-zero-opp
- lt-zero-opp-conv
- lt-zero-opp-equiv
- minus-lt
- minus-lt-conv
- nat-ge-zero
- neg-lt-zero
- neg-lt-zero-conv
- neg-lt-zero-equiv
- ord-int-split
- plus-le
- plus-le-cong
- plus-le-conv
- plus-le-equiv
- plus-lt
- plus-lt-conv
- plus-lt-equiv
- pos-ge-one
- pos-gt-zero
- pos-gt-zero-conv
- pos-gt-zero-equiv
- pos-one-split
latte-integers.plus
The addition defined on ℤ.
Public variables and functions:
- +
- add-prop
- add-unique
- negative-plus
- negative-pos-plus
- negative-pos-plus-conv
- negative-pos-plus-equiv
- plus
- plus-assoc
- plus-assoc-sym
- plus-commute
- plus-left-cancel
- plus-left-cancel-conv
- plus-nat-closed
- plus-one
- plus-pred
- plus-pred-succ
- plus-pred-swap
- plus-pred-sym
- plus-prop
- plus-right-cancel
- plus-right-cancel-conv
- plus-succ
- plus-succ-pred
- plus-succ-swap
- plus-succ-sym
- plus-zero
- plus-zero-swap
- positive-plus
latte-integers.times
The multiplication defined on ℤ.
Public variables and functions:
- *
- mult-prop
- mult-split-zero
- mult-unique
- plus-fun
- times
- times-assoc
- times-assoc-sym
- times-commute
- times-dist-minus
- times-dist-minus-sym
- times-dist-plus
- times-dist-plus-sym
- times-eq-one
- times-eq-one-nat
- times-eq-one-nat-swap
- times-gt-pos
- times-gt-pos-one
- times-le-nat
- times-left-cancel
- times-nat-closed
- times-neg-neg
- times-neg-pos
- times-one
- times-one-swap
- times-opp
- times-opp-opp
- times-pos-neg
- times-pos-pos
- times-pred
- times-pred-swap
- times-pred-swap-sym
- times-pred-sym
- times-prop
- times-right-cancel
- times-succ
- times-succ-swap
- times-succ-swap-sym
- times-succ-sym
- times-zero
- times-zero-swap