For record_projection expressions, if an expression
r is of type t,
and t is a record type
with fields 𝔽ₘ
to 𝔽ₙ, of types
tₘ to tₙ,
then accessing field 𝔽ₖ of
r, where
k ∈ [m, n], results in
a value of type tₖ:
For a record_projection expression
e,
the left hand side of the expression is evaluated, by rule
record_projection_pre, and then
e evaluates to the
value associated with the label k
by rule record_projection_value.