module Record where

module M where

  record A
    : Set
    where
  
    constructor
  
      a
  
open M

record B
  : Set
  where

record C
  : Set
  where

  constructor

    c

x
  : A
x
  = a

y
  : C
y
  = record {}

record D
  (E : Set)
  : Set
  where

record F
  : Set₁
  where

  field

    G
      : Set

    z
      : G