The SUBSORT-DEFN declares its first SORT; it declares the
embedding of this as a subsort of its second SORT, which must
already be declared in the local environment; and it asserts that the
values of the subsort are precisely (the projection of) those values
of the variable VAR from the supersort for which the
FORMULA holds.
The scope of the variable VAR 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
(unless the subsort and supersort are declared to be isomorphic).
A subsort definition SUBSORT-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 ::= ... | SUBSORT-DEFN
SUBSORT-DEFN ::= subsort-defn SORT VAR SORT FORMULA
CoFI Document: LanguageSummary --DRAFT, Version 0.96-- 30 April 1997.
Comments to cofi-language@brics.dk