**Go backward to** 4.1.1.2 Isomorphism Declarations

**Go up to** 4.1.1 Sorts

#### 4.1.1.3 Subsort Definitions

SUBSORT-DEFN ::= subsort-defn SORT VAR SORT FORMULA

A subsort definition `SUBSORT-DEFN` is written:

*s* = { *V*:*s'* **·** *F* }

It provides an explicit specification of the values of the subsort
*s* of *s'*, in contrast to the implicit specification
provided by using subsort declarations and overloaded operation
symbols.

The subsort definition declares the sort *s*; it declares the
embedding of *s* as a subsort of *s'*, which must already be
declared in the local environment; and it asserts that the values of
*s* are precisely (the projection of) those values of the
variable *V* from *s'* for which the formula *F* holds.

The scope of the variable *V* is restricted to the formula
*F*. Any other variables occurring in *F* must be
explicitly declared by enclosing quantifications.

Note that the terms of sort *s'* cannot generally be used as
terms of sort *s*. But they can be explicitly projected to
*s*, using a cast.

CoFI
Document: CASL/Summary-v1.0 -- Version: 1.0 -- 22 October 1998.

Comments to cofi-language@brics.dk