FREE-DATATYPE ::= free-datatype DATATYPE-ITEMS
A list FREE-DATATYPE of free datatype declarations is written:
free types DD1; ... DDn;This construct is only well-formed when all the constructors declared by the datatype declarations are total.
The free datatype declarations declare the same sorts, constructors, and selectors as ordinary datatype declarations. Apart from the sentences that define the values of selectors, the free datatype declarations determine additional sentences requiring [CHANGED:] that the constructors are injective, [] that the ranges of constructors of the same sort are disjoint, that all the declared sorts are generated by the constructors, [CHANGED:] and that the value of applying a selector to a constructor for which it has not been declared is always undefined. [] (The sentences ensure that the models, if any, are the same as for a free extension with the datatype declarations.)
When the alternatives of a free datatype declaration are all constants, the declared sort corresponds to an (unordered) enumeration type.