
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
  field
    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