| | | A.1.5 Array Types |
ARRAY T1 OF T2
This type denotes the domain of arrays with indices of type T1 and values of type T2 (see Section Array Values for the operations supported on arrays).
From the semantic point of view, this type is essentially equivalent to a unary function type. The major difference is that the system understands that, if two arrays are equal, access to these arrays at equal indices yields equal results (the system does not understand the corresponding rule for function applications).
| | | A.1.5 Array Types |