Instances.agda

{-# OPTIONS --cubical-compatible #-}
module Class.Decidable.Instances where

open import Class.Prelude
open import Class.Decidable.Core
open import Class.DecEq.Core

instance

  -- ** deriving from DecEq

  DecEq⇒Dec : ⦃ DecEq A ⦄ → _≡_ {A = A} ⁇²
  DecEq⇒Dec = ⁇² _≟_

  -- ** basic type formers

  Dec-⊥ : ⊥ ⁇
  Dec-⊥ .dec = no λ()

  Dec-⊤ : ⊤ ⁇
  Dec-⊤ .dec = yes tt

  open import Relation.Nullary.Decidable as D

  Dec-→ : ⦃ A ⁇ ⦄ → ⦃ B ⁇ ⦄ → (A → B) ⁇
  Dec-→ .dec = dec D.→-dec dec

  -- ** products

  Dec-× : ⦃ A ⁇ ⦄ → ⦃ B ⁇ ⦄ → (A × B) ⁇
  Dec-× .dec = dec D.×-dec dec

  -- ** sums

  Dec-⊎ : ⦃ A ⁇ ⦄ → ⦃ B ⁇ ⦄ → (A ⊎ B) ⁇
  Dec-⊎ .dec = dec D.⊎-dec dec

  Dec-T : T ⁇¹
  Dec-T = ⁇¹ 𝔹.T?

  import Data.List.Relation.Unary.All as L
  import Data.List.Relation.Unary.Any as L

  Dec-All : ⦃ P ⁇¹ ⦄ → L.All P ⁇¹
  Dec-All = ⁇¹ L.all? dec¹

  Dec-Any : ⦃ P ⁇¹ ⦄ → L.Any P ⁇¹
  Dec-Any = ⁇¹ L.any? dec¹

  import Data.List.Relation.Unary.AllPairs as AP

  Dec-AllPairs : ⦃ R ⁇² ⦄ → AP.AllPairs R ⁇¹
  Dec-AllPairs = ⁇¹ AP.allPairs? dec²

  open import Data.Vec.Relation.Unary.All as V
  open import Data.Vec.Relation.Unary.Any as V

  Dec-VAll : ⦃ P ⁇¹ ⦄ → V.All P {n} ⁇¹
  Dec-VAll = ⁇¹ V.all? dec¹

  Dec-VAny : ⦃ P ⁇¹ ⦄ → V.Any P {n} ⁇¹
  Dec-VAny = ⁇¹ V.any? dec¹

  import Data.Maybe.Relation.Unary.All as Mb renaming (dec to all?)
  import Data.Maybe.Relation.Unary.Any as Mb renaming (dec to any?)

  Dec-MAll : ⦃ P ⁇¹ ⦄ → Mb.All P ⁇¹
  Dec-MAll = ⁇¹ Mb.all? dec¹

  Dec-MAny : ⦃ P ⁇¹ ⦄ → Mb.Any P ⁇¹
  Dec-MAny = ⁇¹ Mb.any? dec¹

  -- ** inequalities

  ℕ-Dec-≤ = ⁇² Nat._≤?_
  ℕ-Dec-< = ⁇² Nat._<?_

  import Data.Integer.Properties as ℤ

  ℤ-Dec-≤ = ⁇² ℤ._≤?_
  ℤ-Dec-< = ⁇² ℤ._<?_

  import Data.Rational.Properties as Rat

  ℚ-Dec-≤ = ⁇² Rat._≤?_
  ℚ-Dec-< = ⁇² Rat._<?_