module Decidable where

open import Equality
open import Level
open import Proposition

----------------------------------------------------------------------
-- Decidable properties
----------------------------------------------------------------------
data Dec {ℓ : Level} (A : Set ℓ) : Set ℓ where
  yes : (x : A)    → Dec A
  no  : (¬x : ¬ A) → Dec A

----------------------------------------------------------------------
-- Decidable equality
----------------------------------------------------------------------
record hasDecEq {ℓ : Level}(A : Set ℓ) : Set ℓ where
  infix  _≐_
  field _≐_ : (x y : A) → Dec (x ≡ y)

open hasDecEq {{...}} public

{-# DISPLAY hasDecEq._≐_ x y = x ≐ y #-}