| | | A.1.3 Subtypes |
SUBTYPE(E)
This type takes a value E of type T -> BOOLEAN for some type T, i.e. a unary predicate on T. The type denotes the domain of all values of T that satisfy this predicate.
The denoted predicate must not be false for all values of T; thus the type gives rise to a type checking condition exist x in T: Ex.
The value E is typically denoted by a function expression.
| | | A.1.3 Subtypes |