[ agda#1332 ] Expose instances for decidable equality

Author: jespercockx

src/Data/Bin/Instances.agda

@@ -0,0 +1,14 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Instances for bits
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Bin.Instances where
+
+open import Data.Bin.Properties
+
+instance
+  ≡-isDecEquivalence-Bin = ≡-isDecEquivalence

src/Data/Bool/Instances.agda

@@ -0,0 +1,16 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Instances for booleans
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Bool.Instances where
+
+open import Data.Bool.Properties
+open import Relation.Binary.PropositionalEquality.Properties
+  using (isDecEquivalence)
+
+instance
+  ≡-isDecEquivalence-Bool = isDecEquivalence _≟_

src/Data/Char/Instances.agda

@@ -0,0 +1,16 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Instances for characters
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Char.Instances where
+
+open import Data.Char.Properties
+open import Relation.Binary.PropositionalEquality.Properties
+  using (isDecEquivalence)
+
+instance
+  ≡-isDecEquivalence-Char = isDecEquivalence _≟_

src/Data/Fin/Instances.agda

@@ -0,0 +1,15 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Instances for finite sets
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Fin.Instances where
+
+open import Data.Fin.Base
+open import Data.Fin.Properties
+
+instance
+  ≡-isDecEquivalence-Fin = ≡-isDecEquivalence

src/Data/Float/Instances.agda

@@ -0,0 +1,16 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Instances for floating point numbers
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Float.Instances where
+
+open import Data.Float.Properties
+open import Relation.Binary.PropositionalEquality.Properties
+  using (isDecEquivalence)
+
+instance
+  ≡-isDecEquivalence-Float = isDecEquivalence _≟_

src/Data/Integer/Instances.agda

@@ -0,0 +1,16 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Instances for integers
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Integer.Instances where
+
+open import Data.Integer.Properties
+open import Relation.Binary.PropositionalEquality.Properties
+  using (isDecEquivalence)
+
+instance
+  ≡-isDecEquivalence-Integer = isDecEquivalence _≟_

src/Data/List/Instances.agda

@@ -9,6 +9,11 @@
 module Data.List.Instances where
 
 open import Data.List.Categorical
+open import Data.List.Properties
+  using (≡-dec)
+open import Relation.Binary.PropositionalEquality.Properties
+  using (isDecEquivalence)
+open import Relation.Binary.TypeClasses
 
 instance
   listFunctor = functor
@@ -19,3 +24,5 @@ instance
   listMonadZero = monadZero
   listMonadPlus = monadPlus
   listMonadT = λ {ℓ} {M} {{inst}} → monadT {ℓ} {M} inst
+
+  ≡-isDecEquivalence-List = λ {a} {A} {{≡-isDecEquivalence-A}} → isDecEquivalence (≡-dec {a} {A} (_≟_ {{≡-isDecEquivalence-A}}))

src/Data/Nat/Binary/Instances.agda

@@ -0,0 +1,16 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Instances for binary natural numbers
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Nat.Binary.Instances where
+
+open import Data.Nat.Binary.Properties
+open import Relation.Binary.PropositionalEquality.Properties
+  using (isDecEquivalence)
+
+instance
+  ≡-isDecEquivalence-ℕᵇ = isDecEquivalence _≟_

src/Data/Nat/Instances.agda

@@ -0,0 +1,16 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Instances for natural numbers
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Nat.Instances where
+
+open import Data.Nat.Properties
+open import Relation.Binary.PropositionalEquality.Properties
+  using (isDecEquivalence)
+
+instance
+  ≡-isDecEquivalence-ℕ = isDecEquivalence _≟_

src/Data/Product/Instances.agda

@@ -0,0 +1,21 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Typeclass instances for products
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Product.Instances where
+
+open import Data.Product.Properties
+open import Relation.Binary.PropositionalEquality.Properties
+  using (isDecEquivalence)
+open import Relation.Binary.PropositionalEquality.Core
+  using (_≡_)
+open import Relation.Binary.Structures
+  using (IsDecEquivalence)
+open import Relation.Binary.TypeClasses
+
+instance
+  ≡-isDecEquivalence-Σ = λ {a} {b} {A} {B} {{≡-isDecEquivalence-A}} {{≡-isDecEquivalence-B : ∀ {a} → IsDecEquivalence (_≡_ {A = B a})}} → isDecEquivalence (≡-dec {a} {A = A} {b} {B = B} (_≟_ {{≡-isDecEquivalence-A}}) (_≟_ {{≡-isDecEquivalence-B}}))

src/Data/Rational/Instances.agda

@@ -0,0 +1,16 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Instances for rational numbers
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Rational.Instances where
+
+open import Data.Rational.Properties
+open import Relation.Binary.PropositionalEquality.Properties
+  using (isDecEquivalence)
+
+instance
+  ≡-isDecEquivalence-ℚ = isDecEquivalence _≟_

src/Data/Sign/Instances.agda

@@ -0,0 +1,16 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Instances for signs
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Sign.Instances where
+
+open import Data.Sign.Properties
+open import Relation.Binary.PropositionalEquality.Properties
+  using (isDecEquivalence)
+
+instance
+  ≡-isDecEquivalence-Sign = isDecEquivalence _≟_

src/Data/String/Instances.agda

@@ -0,0 +1,16 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Instances for strings
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.String.Instances where
+
+open import Data.String.Properties
+open import Relation.Binary.PropositionalEquality.Properties
+  using (isDecEquivalence)
+
+instance
+  ≡-isDecEquivalence-String = isDecEquivalence _≟_

src/Data/Sum/Instances.agda

@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Typeclass instances for sums
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Sum.Instances where
+
+open import Data.Sum.Properties
+open import Relation.Binary.PropositionalEquality.Properties
+  using (isDecEquivalence)
+open import Relation.Binary.TypeClasses
+
+instance
+  ≡-isDecEquivalence-⊎ = λ {a} {b} {A} {B} {{≡-isDecEquivalence-A}} {{≡-isDecEquivalence-B}} → isDecEquivalence (≡-dec {a} {A = A} {b} {B = B} (_≟_ {{≡-isDecEquivalence-A}}) (_≟_ {{≡-isDecEquivalence-B}}))

src/Data/These/Instances.agda

@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Typeclass instances for These
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.These.Instances where
+
+open import Data.These.Properties
+open import Relation.Binary.PropositionalEquality.Properties
+  using (isDecEquivalence)
+open import Relation.Binary.TypeClasses
+
+instance
+  ≡-isDecEquivalence-These = λ {a} {b} {A} {B} {{≡-isDecEquivalence-A}} {{≡-isDecEquivalence-B}} → isDecEquivalence (≡-dec {a} {b} {A = A} {B = B} (_≟_ {{≡-isDecEquivalence-A}}) (_≟_ {{≡-isDecEquivalence-B}}))

src/Data/Unit/Instances.agda

@@ -0,0 +1,16 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Instances for the unit type
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Unit.Instances where
+
+open import Data.Unit.Properties
+open import Relation.Binary.PropositionalEquality.Properties
+  using (isDecEquivalence)
+
+instance
+  ≡-isDecEquivalence-Unit = isDecEquivalence _≟_

src/Data/Vec/Instances.agda

@@ -9,7 +9,16 @@
 module Data.Vec.Instances where
 
 open import Data.Vec.Categorical
+open import Data.Vec.Properties
+  using (≡-dec)
+open import Relation.Binary.PropositionalEquality.Properties
+  using (isDecEquivalence)
+open import Data.Vec.Relation.Binary.Equality.DecPropositional
+open import Relation.Binary.TypeClasses
+
 
 instance
   vecFunctor = functor
   vecApplicative = applicative
+
+  ≡-isDecEquivalence-Vec = λ {a} {A} {{≡-isDecEquivalence-A}} {n} → isDecEquivalence (≡-dec {a} {A} (_≟_ {{≡-isDecEquivalence-A}}) {n})

src/Data/Word/Instances.agda

@@ -0,0 +1,16 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Instances for words
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Word.Instances where
+
+open import Data.Word.Properties
+open import Relation.Binary.PropositionalEquality.Properties
+  using (isDecEquivalence)
+
+instance
+  ≡-isDecEquivalence-Word = isDecEquivalence _≟_

src/Reflection/Instances.agda

@@ -0,0 +1,38 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Instances for reflected syntax
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Reflection.Instances where
+
+import Reflection.Literal as Literal
+import Reflection.Name as Name
+import Reflection.Meta as Meta
+import Reflection.Abstraction as Abstraction
+import Reflection.Argument as Argument
+import Reflection.Argument.Visibility as Visibility
+import Reflection.Argument.Relevance as Relevance
+import Reflection.Argument.Information as Information
+import Reflection.Pattern as Pattern
+import Reflection.Term as Term
+
+open import Relation.Binary.PropositionalEquality.Properties
+  using (isDecEquivalence)
+open import Relation.Binary.TypeClasses
+
+instance
+  ≡-isDecEquivalence-Lit = isDecEquivalence Literal._≟_
+  ≡-isDecEquivalence-Name = isDecEquivalence Name._≟_
+  ≡-isDecEquivalence-Meta = isDecEquivalence Meta._≟_
+  ≡-isDecEquivalence-Visibility = isDecEquivalence Visibility._≟_
+  ≡-isDecEquivalence-Relevance = isDecEquivalence Relevance._≟_
+  ≡-isDecEquivalence-Arg-info = isDecEquivalence Information._≟_
+  ≡-isDecEquivalence-Pattern = isDecEquivalence Pattern._≟_
+  ≡-isDecEquivalence-Abs = λ {ℓ} {A} {{≡-isDecEquivalence-A}} → isDecEquivalence (Abstraction.≡-dec {ℓ} {A} (_≟_ {{≡-isDecEquivalence-A}}))
+  ≡-isDecEquivalence-Arg = λ {ℓ} {A} {{≡-isDecEquivalence-A}} → isDecEquivalence (Argument.≡-dec {ℓ} {A} (_≟_ {{≡-isDecEquivalence-A}}))
+  ≡-isDecEquivalence-Clause = isDecEquivalence Term._≟-Clause_
+  ≡-isDecEquivalence-Term = isDecEquivalence Term._≟_
+  ≡-isDecEquivalence-Sort = isDecEquivalence Term._≟-Sort_

src/Relation/Binary/TypeClasses.agda

@@ -0,0 +1,13 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Typeclasses for use with instance arguments
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Relation.Binary.TypeClasses where
+
+open import Relation.Binary.Structures using (IsDecEquivalence)
+
+open IsDecEquivalence {{...}} public