diff --git a/CHANGELOG.md b/CHANGELOG.md index f83411bc22..7e0df82f36 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -99,6 +99,16 @@ Deprecated names truncate-irrelevant ↦ Relation.Binary.PropositionalEquality.Core.refl ``` +* In `Relation.Binary.Construct.Intersection`: + ```agda + decidable ↦ _∩?_ + ``` + +* In `Relation.Binary.Construct.Union`: + ```agda + decidable ↦ _∪?_ + ``` + * In `Relation.Nullary.Decidable.Core`: ```agda ⊤-dec ↦ ⊤? diff --git a/src/Relation/Binary/Construct/Intersection.agda b/src/Relation/Binary/Construct/Intersection.agda index b5dda5737e..16603994b6 100644 --- a/src/Relation/Binary/Construct/Intersection.agda +++ b/src/Relation/Binary/Construct/Intersection.agda @@ -86,8 +86,10 @@ module _ (≈ : Rel A ℓ₁) (L : Rel A ℓ₂) (R : Rel A ℓ₃) where module _ {L : REL A B ℓ₁} {R : REL A B ℓ₂} where - decidable : Decidable L → Decidable R → Decidable (L ∩ R) - decidable L? R? x y = L? x y ×? R? x y + infixl 6 _∩?_ + + _∩?_ : Decidable L → Decidable R → Decidable (L ∩ R) + _∩?_ L? R? x y = L? x y ×? R? x y ------------------------------------------------------------------------ -- Structures @@ -102,7 +104,7 @@ isEquivalence {L = L} {R = R} eqₗ eqᵣ = record isDecEquivalence : IsDecEquivalence L → IsDecEquivalence R → IsDecEquivalence (L ∩ R) isDecEquivalence eqₗ eqᵣ = record { isEquivalence = isEquivalence L.isEquivalence R.isEquivalence - ; _≟_ = decidable L._≟_ R._≟_ + ; _≟_ = L._≟_ ∩? R._≟_ } where module L = IsDecEquivalence eqₗ; module R = IsDecEquivalence eqᵣ isPreorder : IsPreorder ≈ L → IsPreorder ≈ R → IsPreorder ≈ (L ∩ R) @@ -144,3 +146,18 @@ isStrictPartialOrderʳ {L = L} {≈ = ≈} {R = R} transₗ respₗ Oᵣ = recor ; trans = transitive L R transₗ Oᵣ.trans ; <-resp-≈ = respects₂ ≈ L R respₗ Oᵣ.<-resp-≈ } where module Oᵣ = IsStrictPartialOrder Oᵣ + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- version 2.4 + +decidable = _∩?_ +{-# WARNING_ON_USAGE decidable +"Warning: decidable was deprecated in v2.4. +Please use _∩?_ instead." +#-} diff --git a/src/Relation/Binary/Construct/Union.agda b/src/Relation/Binary/Construct/Union.agda index a99c54dd1b..1096242437 100644 --- a/src/Relation/Binary/Construct/Union.agda +++ b/src/Relation/Binary/Construct/Union.agda @@ -84,5 +84,22 @@ module _ (≈ : REL A B ℓ₁) (L : REL A B ℓ₂) (R : REL A B ℓ₃) where module _ {L : REL A B ℓ₁} {R : REL A B ℓ₂} where - decidable : Decidable L → Decidable R → Decidable (L ∪ R) - decidable L? R? x y = L? x y ⊎? R? x y + infixr 6 _∪?_ + + _∪?_ : Decidable L → Decidable R → Decidable (L ∪ R) + _∪?_ L? R? x y = L? x y ⊎? R? x y + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- version 2.4 + +decidable = _∪?_ +{-# WARNING_ON_USAGE decidable +"Warning: decidable was deprecated in v2.4. +Please use _∪?_ instead." +#-}