knock-on: tighten impports

agda · Oct 1, 2024 · ec7494f · ec7494f
1 parent 6263040
commit ec7494f
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/src/Data/List/Relation/Binary/Subset/DecSetoid.agda b/src/Data/List/Relation/Binary/Subset/DecSetoid.agda
@@ -14,10 +14,10 @@ open import Function.Base using (_∘_)
 open import Data.List.Base using ([]; _∷_)
 open import Data.List.Relation.Unary.Any using (here; there; map)
 open import Relation.Binary.Definitions using (Decidable)
-open import Relation.Nullary using (yes; no)
-open DecSetoid S
-open import Data.List.Relation.Binary.Equality.DecSetoid S
-open import Data.List.Membership.DecSetoid S
+open import Relation.Nullary.Decidable.Core using (yes; no)
+
+open DecSetoid S using (setoid; refl; trans)
+open import Data.List.Membership.DecSetoid S using (_∈?_)
 
 -- Re-export definitions
 open import Data.List.Relation.Binary.Subset.Setoid setoid public