If you want to get the value of certain field in a record, you use the ``.'' operator. For example,
[ x:= 0, y := 1 ].x;evaluates to 0.
You may construct new records from old using the « operator. For example,
[ x:= 0, y := 1 ] << [ x := -1 ]evaluates to [ x := -1, y := 1 ]. More generally, the expression r « s has all fields appearing in either r or s. The value associated with the a particular field x in r « s is s.x if x exists in s, and otherwise it is r.x. If r and s have a field name in common but do not assign that field a value of the same type, a type error is produced.