This report describes the current LEGO library, which was designed as
a basis upon which users can develop their own work, and also some
example proof developments using this library. An earlier version of
the library was developed by Savi Maharaj for use by students being
introduced to the
LEGO system. We hope
that this version will provide useful preliminaries for *all*
users.

We have received contributions from: Thorsten Altenkirch; Petr Cizek; Adriana Compagnoni; Healf Goguen; Martin Hofmann; Claire Jones; Zhaohui Luo; Savi Maharaj; Conor McBride; James McKinna; Randy Pollack; Thomas Schreiber.

The LEGO library contains around 250 definitions and 400 theorems, and covers both the common datatypes such as natural numbers, list, booleans, products, sums, unit, empty and some more unusual ones such as integers, sigma types, quotient types, finite sets, vectors. New modules have been incorporated offering

- abstract data types
- a theory of relations
- a new theory of permutations
- a theory of sorted lists
- theorems on divisions
- theorems on exponentiation

The library exploits LEGO's module
system so that loading a library file will
automatically load the files on which it depends and
two library files which depend on
some common files will have the common files loaded
only once. So users don't need to know anything about the
dependency structure of the library, only where to find
the theorems they want. For faster loading, the library also stores
``compiled'' versions of most files which can be accessed by using
the `Make`

command in LEGO.