Reconciles Data.Vec.Relation.Binary.Equality.DecPropositional with List (#2451)

Author: jamesmckinna

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)
+  ```

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 _≟_