Latte-prelude 1.0b10-SNAPSHOT
Released under the MIT Licence
The core library for the LaTTe proof assistant.
Installation
To install, add the following dependency to your project or build file:
[latte-prelude "1.0b10-SNAPSHOT"]
Namespaces
latte-prelude.classic
The axioms of classical logic, and basic derived proof rules.
Public variables and functions:
latte-prelude.equal
The formal definition of equality, and its basic properties.
Public variables and functions:
latte-prelude.fun
A function with domain T and codomain U has type (==> T U).
Public variables and functions:
- <<
- >>
- bijective
- bijective-is-injective
- bijective-is-surjective
- bijective-unique
- codomain
- compose
- compose-injective
- domain
- fun-equal-ext
- functional-extensionality
- identity
- injective
- injective-single
- inverse
- inverse-bijective
- inverse-injective
- inverse-prop
- inverse-prop-conv
- inverse-surjective
- law-associativity
- law-identity-left
- law-identity-right
- point
- retraction
- section
- solve-section
- surjective
- Unit
- unit
latte-prelude.prop
Basic definitions and theorems for (intuitionistic) propositional logic. Most natural deduction rules are provided as theorems in this namespace.
Public variables and functions:
- <=>
- absurd
- absurd-intro
- and
- and*
- and*-arity
- and-elim*
- and-elim-left
- and-elim-left-thm
- and-elim-right
- and-elim-right-thm
- and-intro
- and-intro*
- and-intro-thm
- and-sym
- and-sym-thm
- and-unparser
- build-and-elim
- build-and-intros-left-leaning
- build-and-intros-right-leaning
- build-or-elim*
- build-or-intro
- build-r-and-elim
- decompose-and-type
- decompose-iff-type
- decompose-impl-type
- decompose-lambda-term
- decompose-or-type
- elim-path
- ex-falso
- iff-elim-if
- iff-elim-if-thm
- iff-elim-only-if
- iff-elim-only-if-thm
- iff-intro
- iff-intro-thm
- iff-refl
- iff-sym
- iff-sym-thm
- iff-trans
- iff-trans-thm
- impl-ignore
- impl-not-not
- impl-refl
- impl-trans
- impl-trans-thm
- mk-nary-op-left-leaning
- mk-nary-op-right-leaning
- not
- or
- or*
- or-assoc
- or-assoc-conv-thm
- or-assoc-thm
- or-elim
- or-elim*
- or-elim-thm
- or-intro*
- or-intro-left
- or-intro-left-thm
- or-intro-right
- or-intro-right-thm
- or-not-elim-left
- or-not-elim-right
- or-not-impl-elim
- or-sym
- or-sym-thm
- or-unparser
- r-and*
- r-and-elim*
- r-and-intro*
- truth
- truth-is-true
latte-prelude.quant
Basic definitions and theorems about the universal and existential quantifiers.