| | | A.2.10 Record Values, Updates, and Selections |
(# I1:=E1, I2:=E2, ...,
In:=En #)
E WITH [I1]:=E1
E WITH [I2]:=E2
...
E WITH [In]:=En
E.I1
E.I2
...
E.In
The record value expression
(# I1:=E1, I2:=E2, ..., In:=En #)
denotes the n-ary record composed of the values of E1, E2, ..., En by assigning these values to the record field identifiers I1, I2, ..., In. Correspondingly the type of the expression is the record type (# I1:T1, I2:T2, ..., In:Tn #) where T1 is the type of E1, T2 is the type of E2, ..., Tn is the type of En.
The n record update expressions E WITH [I1]:=E1, E WITH [I2]:=E2, ..., E WITH [In]:=En each take a value expression E of record type (# I1:T1, I2:T2, ..., In:Tn #) for some identifiers I1, I2, ..., In and types T1, T2, ..., Tn and one of the values E1 of type T1, E2 of type T2, ..., En of type Tn. They denote the record that is identical to E except that record field I1, I2, ..., In is updated by value E1, E2, ..., En. Correspondingly the type of each expression is also (# I1:T1, I2:T2, ..., In:Tn #).
The n record selection expressions E.I1, E.I2, ..., E.In take a value E of record type (# I1:T1, I2:T2, ..., In:Tn #) for some identifiers I1, I2, ..., In and types T1, T2, ..., Tn. The expressions denote the first, second, ..., n-th component of this record; their types are T1, T2, ..., Tn, correspondingly.
| | | A.2.10 Record Values, Updates, and Selections |