A.1.7 Record Types

A.1.7 Record Types

Synopsis

Description

This type denotes the domain of n-ary records (# I₁:=a₁, I₂:=a₂, ..., I_n:=a_n #) with n values a₁ from T1, a₂ from T2, ..., a_n from Tn assigned to record field identifiers I₁, I₂, ..., I_n (see Section Record Values for the operations supported on records).

A.1.7 Record Types