Latte-prelude 1.0b7-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.0b7-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.

latte-prelude.fun

A function with domain T and codomain U has type (==> T U).

latte-prelude.prop

Basic definitions and theorems for (intuitionistic) propositional logic. Most natural deduction rules are provided as theorems in this namespace.

latte-prelude.quant

Basic definitions and theorems about the universal and existential quantifiers.