After the Agda Records Tutorial

module Modules.Records where

open import Data.Nat
open import Data.Bool
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

Record modules

Record defines modules similar to data definitions but these modules are not automatically opened:

record R : Set where
    r₁ : Bool
    r₂ : 

x : R
x = record { r₁ = true; r₂ = 2 }

We can open R:

module SimpleOpening where

  open R  -- brings r₁ and r₂ into scope

  y : Bool
  y = r₁ x  -- no qualification

Applied opening

Applied opening also works for R:

module AppliedOpening where

  open R x  -- brings r₁ and r₂ into scope, first parameter filled in 

  y : Bool
  y = r₁

Another example:

module AppliedOpening′ where

  y : Bool
  y = r₁ where
    open R x