The Micro Library

This library collects very basic theories concerning the most commonly used sets together with some elementary properties. It may be imported alltogether invoking Import on m icrolib. A c ore theory provides an implementation of the sets presented in [], though without the constants corresponding to the elimination rules. The theory r el provides constants to characterize binary relations, it formally defines what it means for a binary relation to be reflexive, symmetric, transitive, decidable, total and defines the accessible part of a relation. In the theory i d properties of propositional equality are proved. The theory a lgebra contains definitions characterizing semigroups, monoids and commutative monoids. The theories n at , l ists and v ec define natural numbers, lists and arrays, toghether with some functions, relations and properties of these. We now list the theories of the microlibrary. In this list, the primitive constants are shown as they stand, but for the defined constants only the name and typing is shown (the definitions themselves have been hidden, one may inspect them by importing the theories). In writing this library we have followed the following conventions:

1. names of sets start with a capital letter,
2. names of elements of sets start with a small letter,
3. different words in a name are commenced with a capital letter,
4. for sets with one constructor the same name is used both for the set and the constructor.

core

rel, simple properties of relations.

id, simple properties of propositional equality.

algebra, algebraic terminology.

nat, simple properties of natural numbers.

lists, simple properties of lists.

vec, vectors.