| | | A.1.2 Range Types |
[E1..E2]
This type takes two expressions E1 and E2 denoting integer values such that the value of E1 is less than or equal the value of E2; the type denotes the domain of all integers greater than or equal E1 and less than or equal E2.
The type gives rise to a type checking condition E1 <= E2.
This type is essentially equivalent to the subtype
SUBTYPE(LAMBDA(x:INT): E1 <= x AND x <= E2)
| | | A.1.2 Range Types |