agda-unused-0.1.0: data/test/declaration/Record.agda

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 {}