| | | A.2.9 Tuple Values, Updates, and Selections |
(E1, E2, ..., En)
E WITH [0]:=E1
E WITH [1]:=E2
...
E WITH [n-1]:=En
E.0
E.1
...
E.n-1
The tuple value expression (E1, E2, ..., En) denotes the n-ary tuple composed of the values E1, E2, ..., En. Correspondingly the type of the expression is the tuple type (T1, T2, ..., Tn) where T1 is the type of E1, T2 is the type of E2, ..., Tn is the type of En. The tuple (E) is identified with E.
The n tuple update expressions E WITH [0]:=E1, E WITH [1]:=E2, ..., E WITH [n-1]:=En each take a value E of tuple type (T1,T2,...,Tn) for some types T1, T2, ..., Tn and one of the values E1 of type T1, E2 of type T2, ..., En of type Tn. They denote the tuple that is identical to E except that component 0, 1, ..., n-1 is updated by value E1, E2, ..., En. Correspondingly the type of each expression is also (T1,T2,...,Tn).
The n tuple selection expressions E.0, E.1, ..., E.n-1 each take a value E of tuple type (T1,T2,...,Tn) for some types T1, T2, ..., Tn. The expressions denote the first, second, ..., n-th component of this tuple; their types are T1, T2, ..., Tn, correspondingly.
| | | A.2.9 Tuple Values, Updates, and Selections |