4.15.7 Record functor

4.15.7.1 Select function

The select function of the record lattice functor recursively calls the select functions of the lattices corresponding to its features.

4.15.7.2 Make variable function

The make variable function of the record lattice functor recursively calls the make variable functions of the lattices corresponding to its features.

4.15.7.3 Count function

The count function returns:

     o(fd: FDI
       fs: FSI)

where FDI is the sum of the finite domain variables counted for the co-domains of the record, and FSI the sum of the finite set variables.

4.15.7.4 Additional interface features

Below, we show the additional interface features of this lattice:

     record: ALatRec

The record feature is a record representing mapping the fields in the arity of the record (A) to the lattices corresponding to their types (Lat).