The PRED-SORT-DEFN declares the first SORT; it declares the
embedding of this as a subsort of the second SORT, which must
already be declared in the local environment; and it asserts that the
values of the subsort are precisely (the projections of) those values
of the variable VAR from the supersort for which the FORMULA holds.
The variable VAR must occur in the FORMULA, and its scope is
restricted to the FORMULA. Any other variables occurring in the
FORMULA must be explicitly declared by enclosing quantifications.
Note that the only terms of the supersort that are also in the subsort
are explicit projections, expressed using the CAST construct
(described in the next section).
A predicative sort definition PRED-SORT-DEFN determines the
values of a new subsort of a previously-declared sort, by taking just
those values for which a formula holds. It provides an explicit
specification of the values of a subsort, in contrast to the implicit
specification provided by using subsort declarations and overloaded
function symbols.
BASIC-ITEM ::= ... | PRED-SORT-DEFN
PRED-SORT-DEFN ::= pred-sort-defn SORT VAR SORT FORMULA
CoFI Tentative Document: LanguageSummary --Version 0.95-- March 6, 1997.
Comments to cofi-language@brics.dk