Reconciles Data.Vec.Relation.Binary.Equality.DecPropositional with …

…`List` (#2451)
agda · Aug 12, 2024 · c00030a · c00030a
1 parent 04f9d1c
commit c00030a
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 0 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -36,3 +36,8 @@ Additions to existing modules
   ```agda
   map-concat : map f (concat xss) ≡ concat (map (map f) xss)
   ```
+
+* In `Data.Vec.Relation.Binary.Equality.DecPropositional`:
+  ```agda
+  _≡?_ : DecidableEquality (Vec A n)
+  ```
diff --git a/src/Data/Vec/Relation/Binary/Equality/DecPropositional.agda b/src/Data/Vec/Relation/Binary/Equality/DecPropositional.agda
@@ -11,6 +11,8 @@ open import Relation.Binary.Definitions using (DecidableEquality)
 module Data.Vec.Relation.Binary.Equality.DecPropositional
   {a} {A : Set a} (_≟_ : DecidableEquality A) where
 
+open import Data.Vec.Base using (Vec)
+open import Data.Vec.Properties using (≡-dec)
 import Data.Vec.Relation.Binary.Equality.Propositional as PEq
 import Data.Vec.Relation.Binary.Equality.DecSetoid as DSEq
 open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
@@ -22,3 +24,11 @@ open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
 open PEq public
 open DSEq (decSetoid _≟_) public
   using (_≋?_; ≋-isDecEquivalence; ≋-decSetoid)
+
+------------------------------------------------------------------------
+-- Additional proofs
+
+infix 4 _≡?_
+
+_≡?_ : ∀ {n} → DecidableEquality (Vec A n)
+_≡?_ = ≡-dec _≟_