Next: Equality
Up: Customising the Library
Previous: Customising the Library
Given an inductive definition of a type I, one can exploit its
generated elimination principle to define functions with domain I.
The range of such a definition is limited by the universe of the
elimination principle i.e., Prop, Type(i) or
Type. Recall that Prop
Type(i)
Type. Hence, the theories
of inductive definition vary according to the choice of universe. In
particular, one cannot prove disjointness of constructors for any
inductive definition which is eliminated over the kind Prop.
The environmental variable LEGOPATH controls the search path
for LEGO modules. By default it accommodates elimination over
Type and inductive types inhabiting Type. It is set to
.:$LIBDIR/lib_Type:$LIBDIR where LIBDIR records
the root directory of the library.
Users who prefer elimination over
- Prop
- need to replace lib_Type by
lib_Prop in their LEGOPATH. In this
configuration, inductive types inhabit the kind Prop.
- Type(2)
- need to replace lib_Type by
lib_TYPE in their LEGOPATH. In this
configuration, inductive types inhabit the kind Type(0)
More exotic configurations can be achieved by setting the variables
SET, TYPE, TYPE_minus1, and TYPE_minus2 in a
module called parameters and ensure that
- their LEGOPATH considers their version of
parameters before any such module in the library
- LEGOPATH has to include lib_TYPE.
Inductive types inhabit SET and the elimination rule
eliminates over TYPE. Notice that some theorems in the
library fail unless TYPE_minus2 : TYPE_minus1 :
TYPE.
Next: Equality
Up: Customising the Library
Previous: Customising the Library
Lego
1998-06-15