From 2ffc3b062c7fe30c00ffc1624ee8c9518b6c964e Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 1 Oct 2024 12:04:34 +0100 Subject: [PATCH 1/4] refactor `Data.List.Relation.Binary.Equality.DecSetoid` --- .../Relation/Binary/Equality/DecSetoid.agda | 27 +++++++------------ 1 file changed, 9 insertions(+), 18 deletions(-) diff --git a/src/Data/List/Relation/Binary/Equality/DecSetoid.agda b/src/Data/List/Relation/Binary/Equality/DecSetoid.agda index 670e3c981b..00c0d1bf82 100644 --- a/src/Data/List/Relation/Binary/Equality/DecSetoid.agda +++ b/src/Data/List/Relation/Binary/Equality/DecSetoid.agda @@ -7,33 +7,24 @@ {-# OPTIONS --cubical-compatible --safe #-} open import Relation.Binary.Bundles using (DecSetoid) -open import Relation.Binary.Structures using (IsDecEquivalence) -open import Relation.Binary.Definitions using (Decidable) module Data.List.Relation.Binary.Equality.DecSetoid {a ℓ} (DS : DecSetoid a ℓ) where import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality -import Data.List.Relation.Binary.Pointwise as PW -open import Level -open import Relation.Binary.Definitions using (Decidable) -open DecSetoid DS - ------------------------------------------------------------------------- --- Make all definitions from setoid equality available - -open SetoidEquality setoid public +open import Data.List.Relation.Binary.Pointwise using (decSetoid) ------------------------------------------------------------------------ -- Additional properties -infix 4 _≋?_ +≋-decSetoid : DecSetoid _ _ +≋-decSetoid = decSetoid DS -_≋?_ : Decidable _≋_ -_≋?_ = PW.decidable _≟_ +open DecSetoid ≋-decSetoid public + using (setoid) + renaming (isDecEquivalence to ≋-isDecEquivalence; _≟_ to _≋?_) -≋-isDecEquivalence : IsDecEquivalence _≋_ -≋-isDecEquivalence = PW.isDecEquivalence isDecEquivalence +------------------------------------------------------------------------ +-- Make all definitions from setoid equality available -≋-decSetoid : DecSetoid a (a ⊔ ℓ) -≋-decSetoid = PW.decSetoid DS +open SetoidEquality setoid public From 58f043b779d3a5a644547e566d664b6c0416fbfa Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 1 Oct 2024 12:11:25 +0100 Subject: [PATCH 2/4] refactor `Data.List.Relation.Binary.Equality.Setoid` --- .../List/Relation/Binary/Equality/Setoid.agda | 23 +++++++------------ 1 file changed, 8 insertions(+), 15 deletions(-) diff --git a/src/Data/List/Relation/Binary/Equality/Setoid.agda b/src/Data/List/Relation/Binary/Equality/Setoid.agda index f245eeaa5e..76ccc97cfb 100644 --- a/src/Data/List/Relation/Binary/Equality/Setoid.agda +++ b/src/Data/List/Relation/Binary/Equality/Setoid.agda @@ -48,24 +48,17 @@ open PW public -- Relational properties ------------------------------------------------------------------------ -≋-refl : Reflexive _≋_ -≋-refl = PW.refl refl - -≋-reflexive : _≡_ ⇒ _≋_ -≋-reflexive ≡.refl = ≋-refl - -≋-sym : Symmetric _≋_ -≋-sym = PW.symmetric sym - -≋-trans : Transitive _≋_ -≋-trans = PW.transitive trans - -≋-isEquivalence : IsEquivalence _≋_ -≋-isEquivalence = PW.isEquivalence isEquivalence - ≋-setoid : Setoid _ _ ≋-setoid = PW.setoid S +open Setoid ≋-setoid public + using () + renaming ( refl to ≋-refl + ; reflexive to ≋-reflexive + ; sym to ≋-sym + ; trans to ≋-trans + ; isEquivalence to ≋-isEquivalence) + ------------------------------------------------------------------------ -- Relationships to predicates ------------------------------------------------------------------------ From 6263040b1c2c66d65f15c2299a8efe2222b25808 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 1 Oct 2024 12:42:20 +0100 Subject: [PATCH 3/4] oops! get import/export of `setoid` correctt --- src/Data/List/Relation/Binary/Equality/DecSetoid.agda | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Data/List/Relation/Binary/Equality/DecSetoid.agda b/src/Data/List/Relation/Binary/Equality/DecSetoid.agda index 00c0d1bf82..d0c4ab6923 100644 --- 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 _≋?_) ------------------------------------------------------------------------ From ec7494ff1f8a7c062d1ad009c9e8daac6e7f6773 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 1 Oct 2024 13:14:47 +0100 Subject: [PATCH 4/4] 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