A record type is declared as follows:

record R Δ : Set where field x_{1}: A_{1}x_{2}: A_{2}[x_{1}] ... x_{n}: A_n[x_{1}... x_{n-1}]

where `x`

..._{1}`x`

are the fields of the record. Note that the types of later fields can depend on the values of the previous fields.
_{n}

Two things that one might want for a record type are suitably named projection functions and some way of
opening a record to bring the fields into scope. It turns out that using the
module system we can get both things for the price of one. For the record R above,
we generate a parametrised module `R`

module R {Δ}(r : R Δ) where x_{1}: A_{1}x_{1}= ... x_{2}: A_{2}[x_{1}] x_{2}= ... ... x_{n}: A_{n}[x_{1}... x_{n-1}] x_{n}= ...

The functions in `R`

are exactly the projection functions for the record type
`R`

. For instance, we have `R.x`

. (So,
what in some languages is written _{2} : {Δ}(r : R Δ) -> A_{2}[R.x_{1} r]`r.x`

for _{2}`r : R`

, we write as `R.x`

.)
Here it is clear that we want the parameters to the record to be implicit
regardless of whether they are implicit arguments to the record or not. Now the
nice thing is that we can apply the module to a given record, effectively
projecting all fields from the record at once, which is exactly what we are
looking for in a record open feature. So to open a record _{2} r`r : R`

we simply say

open module M = R r

See examples/lattice for an example of how to use the module system and the record types together.