The reference variable the_type_definitions holds a list of entries, one for
each type definition made so far with new_type_definition. It is not normally
explicitly manipulated by the user, but is automatically augmented by each call
of new_type_definition. Each entry contains three strings (the type name,
type constructor name and destructor name) and two theorems (the input
nonemptiness theorem and the returned type bijections). That is, for a call:
Note that the entries made using other interfaces to
new_basic_type_definition, such as define_type, are not included in this
list.
FAILURE CONDITIONS
Not applicable.
USES
This is mainly intended for internal use in new_type_definition, so that
repeated instances of the same definition are ignored rather than rejected.
Some users may find the information useful too.