# Alfa Libraries

Proof development can be speed up dramatically bu using libraries of re-usable proofs, just like program development can be speed up by using libraries of program components. Alfa should of course be accompanied by a large set of standard libraries...

## Libraries

Michael Hedberg is working on a New standard library for Alfa. It is included in Alfa distribution dated 2002-08-01 or later. Documentation is under preparation.

## Examples

Some example files are available. They can be found by clicking on the Library button in the file selection window when opening a file in Alfa.

At present, the following modules are available:

Bool Defines the type `Bool` for booleans (truth values) and some functions. Defines the proposition that a boolean is true. Defines a type for disjount sum and some associeated functions. Basic combinators and function composition. A type for optional values and associated functions. A type for natural numbers, addition, multiplication and equality. Properties of natural numbers, mainly that both addition and multiplication are associative and commutative. A type for cartesian products, the funcions curry and uncurry. Connectives and inferences rules for predicate calculus. Defines the type Prop (for propositions as types), the trivially true proposition and the false (absurd) proposition. Connectives and inference rules for propositional calculus. Standalone, functional programming example. Defines the type `Bool`, the type `Nat` and the functions even and odd from `Nat` to `Bool`. (Used in Keyboard tutorial.) The power of dependent types, compared with Haskell. Sample natural deduction style proofs of some propositions in predicate logic. Sample natural deduction style proofs of some propositions in propositional calculus.
Naming convensions in these examples were inspired by Haskell.
5 Jul 2012 19:45 Thomas Hallgren