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.