From ec7494ff1f8a7c062d1ad009c9e8daac6e7f6773 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 1 Oct 2024 13:14:47 +0100 Subject: [PATCH] knock-on: tighten `impport`s --- src/Data/List/Relation/Binary/Subset/DecSetoid.agda | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Data/List/Relation/Binary/Subset/DecSetoid.agda b/src/Data/List/Relation/Binary/Subset/DecSetoid.agda index fcff0abacc..4bb02f5c0b 100644 --- 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