oops! get import/export of setoid correctt

agda · Oct 1, 2024 · 6263040 · 6263040
1 parent 58f043b
commit 6263040
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/Data/List/Relation/Binary/Equality/DecSetoid.agda b/src/Data/List/Relation/Binary/Equality/DecSetoid.agda
@@ -13,6 +13,7 @@ module Data.List.Relation.Binary.Equality.DecSetoid
 
 import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality
 open import Data.List.Relation.Binary.Pointwise using (decSetoid)
+open DecSetoid DS using (setoid)
 
 ------------------------------------------------------------------------
 -- Additional properties
@@ -21,7 +22,7 @@ open import Data.List.Relation.Binary.Pointwise using (decSetoid)
 ≋-decSetoid = decSetoid DS
 
 open DecSetoid ≋-decSetoid public
-  using (setoid)
+  using ()
   renaming (isDecEquivalence to ≋-isDecEquivalence; _≟_ to _≋?_)
 
 ------------------------------------------------------------------------