next up previous contents
Next: Customizing the Library Up: The LEGO library Previous: Introduction


Currently the root directory of the library is LEGOLIB=/usr/local/share/lego/lib and the environmental variable LEGOPATH controls the search path for LEGO modules, the default value being .:$LEGOLIB/lib_Type:$LEGOLIB:$LEGOLIB/lib_all. This contains various files and subdirectories which most have been given names beginning with the string lib_, in order to avoid name clashes with users' own files. The subdirectory lib_all contains links to all standard modules of the library. Each section in this document, from 5.2 onwards, describes the contents of one subdirectory in the library.

The syntax used in the file listings is the usual LEGO syntax. The types given are always the types produced when the library file is loaded. The notation ``...'' indicates omission of a proof term. Generally the only declarations which have been added to the context are the data-type constructors and elimination rules; all else is derived. The exceptions are in the definition of the quotient type.

Fri May 24 19:01:27 BST 1996