------------------------------------------------------------------------ -- The Agda standard library -- -- This module is DEPRECATED, please use `Data.Record` directly. ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} open import Relation.Binary using (Decidable) open import Relation.Binary.PropositionalEquality using (_≡_) module Record {ℓ} (Label : Set ℓ) (_≟_ : Decidable {A = Label} _≡_) where open import Data.Record Label _≟_ public