At present the library supports three definitions of (substitutive) equality: impredicative (Leibniz) equality and two versions of inductive equality. The library also allows the user to change the universe in which datatypes are defined, and the level over which their elimination rules can range.
The user chooses an equality by simply loading a library equality from those discussed below. It is also possible for a user to create their own equality file. Note that the equality files also configure the LEGO command Qrepl.
The universe levels are controlled by setting various LEGO variables before loading the library files. There are currently four variables: SET, TYPE, TYPE_minus1, and TYPE_minus2.
All inductive datatypes are put in the type universe given by the value of SET; furthermore equality Eq is also defined over this type level. This variable can be set to any type universe level, including Prop.
All inductive datatypes have an elimination rule which is quantified over some expression of the form datatype -> TYPE. The value of TYPE can be chosen by the user to be any universe level. However we warn that many library file won't work if TYPE is set to Prop. See the final paragraph of this section for how to customize the library to work with TYPE as Prop.
A small number of library files also use the type universe variables TYPE_minus1 and TYPE_minus2, which should be set to universe levels strictly below TYPE. As the names imply, TYPE_minus2 should be set to a level strictly below TYPE_minus1.
The library files on finite sets and vectors require certain restrictions to be imposed on the values assigned to the type universe variables. In both these files TYPE_minus2 must be at least Type(0), and consequently TYPE_minus1 must be at least Type(1) and TYPE must be at least Type(2). Type_minus1 is also used in the definition of inductive equality where its value can be any type universe including Prop.
To exploit typical ambiguity [Harper and Pollack, 1991],
defintions
need to be
expanded as macros. Unfortunately, this is not feasable. To
patch this problem, another subdirectory lib_Type has been
provided which contains variants of other modules where all parameters
have been replaced by Type. For convenience, these modules are
accessed in the default path.
For the user who wishes to work with TYPE set to Prop, we give separate versions of four of the library files which include the single assumption true_not_false that the two boolean values true and false are not equal. These files can be loaded in preference to the standard ones by adding (the full pathname of) the top-level library directory lib_prop before the root of the library in the environment variable LEGOPATH. For example, if the library is held in $LEGOLIB then LEGOPATH should be set to
$LEGOLIB/lib_prop:$LEGOLIB:$LEGOLIB/lib_all
(plus any other directories, of course; the current working directory . being most usual). With this set-up, all the library files except vectors and finite sets will work.