At present, the following modules are available:
Bool  Defines the type Bool for booleans (truth values) and some functions.


BoolProp  Defines the proposition that a boolean is true. 
Either  Defines a type for disjount sum and some associeated functions. 
Functions  Basic combinators and function composition. 
Maybe  A type for optional values and associated functions. 
Nat  A type for natural numbers, addition, multiplication and equality. 
NatProp  Properties of natural numbers, mainly that both addition and multiplication are associative and commutative. 
Pair  A type for cartesian products, the funcions curry and uncurry. 
Predikatlogik  Connectives and inferences rules for predicate calculus. 
Prop  Defines the type Prop (for propositions as types), the trivially true proposition and the false (absurd) proposition. 
Satslogik  Connectives and inference rules for propositional calculus. 
evenodd  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.)

localQuant  The power of dependent types, compared with Haskell. 
predikatlogikExempel  Sample natural deduction style proofs of some propositions in predicate logic. 
satslogikExempel  Sample natural deduction style proofs of some propositions in propositional calculus. 