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:

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

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.

Wed Mar 20 13:05:14 MET 1996