[ breaking ] change fieldname _≟_ to _≈?_ in IsDecEquivalence

CHANGELOG.md

@@ -29,6 +29,17 @@ Bug-fixes
 Non-backwards compatible changes
 --------------------------------
 
+* The notation for `Decidable` relations has been (partially) standardised: thus
+  - `_≡?_` (at `infix 4`) for `DecidableEquality`
+  - `_≈?_` (ditto.) for the fieldname of the general `IsDecEquivalence`
+
+  Despite being non-backwards compatible, because a fieldname has changed, the
+  old notation `_≟_` (which was used for both of the above) has been retained,
+  but deprecated. This leads to a large amount of (trivial) deprecations, in
+  addition to the substantive one under `Relation.Binary.Structures`, and in
+  `Data.{Nat|Fin}.Properties` for the concrete datatypes. These deprecations
+  are summarised below, but are not each documented for each affected module.
+
 * [issue #2547](https://github.com/agda/agda-stdlib/issues/2547)
   The names of the *implicit* binders in the following definitions have been
   rectified to be consistent with the rest of `Relation.Binary.Definitions`:
@@ -39,6 +50,7 @@ Non-backwards compatible changes
   `Algebra.*`, the field name of the basic homomorphism property `homo` in
   `Algebra.Morphism.Structures.IsMagmaHomomorphism` has been renamed to `∙-homo`.
 
+
 Minor improvements
 ------------------
 
@@ -59,7 +71,7 @@ Deprecated names
   inj⇒≟    ↦  inj⇒≡?
   ≟-≡      ↦  ≡?-≡
   ≟-≡-refl ↦  ≡?-≡-refl
-  ≟-≢     ↦  ≡?-≢
+  ≟-≢      ↦  ≡?-≢
   ```
 
 * In `Data.Integer.GCD`:
@@ -96,6 +108,22 @@ Deprecated names
   ≢-≟-identity     ↦   ≢-≡?-identity
   ```
 
+* In `Effect.Monad.Partiality`:
+  ```agda
+  _≟-Kind_     ↦   _≡?-Kind_
+  ```
+
+* In `Reflection.AST.AlphaEquality`:
+  ```agda
+  ≟⇒α     ↦   ≡?⇒α
+  ```
+
+* In `Relation.Binary.PropositionalEquality`:
+  ```agda
+  ≡-≟-identity     ↦   ≡-≡?-identity
+  ≢-≟-identity     ↦   ≢-≡?-identity
+  ```
+
 * In `Relation.Nary`:
   ```agda
   ≟-mapₙ     ↦   ≡?-mapₙ

doc/style-guide.md

@@ -590,7 +590,7 @@ word within a compound word is capitalized except for the first word.
   where `R` is the underlying property being asserted to be `Decidable`,
   moreover typically sharing the same fixity and precedence as `R`: thus
   - `_≡?_` (at `infix 4`) for `DecidableEquality`
-  - `_≈?_` (ditto.) for the name of the general `IsDecEquivalence`
+  - `_≈?_` (ditto.) for the fieldname of the general `IsDecEquivalence`
 
 * Any exceptions to these conventions should be flagged on the GitHub
   `agda-stdlib` issue tracker in the usual way.

src/Data/Bool/Properties.agda

@@ -139,7 +139,7 @@ true  ≤? true  = yes b≤b
 ≤-isDecTotalOrder : IsDecTotalOrder _≡_ _≤_
 ≤-isDecTotalOrder = record
   { isTotalOrder = ≤-isTotalOrder
-  ; _≟_          = _≡?_
+  ; _≈?_         = _≡?_
   ; _≤?_         = _≤?_
   }
 

src/Data/Char/Properties.agda

@@ -179,7 +179,7 @@ _≤?_ = Refl.decidable <-cmp
 ≤-isDecPartialOrder : IsDecPartialOrder _≡_ _≤_
 ≤-isDecPartialOrder = record
   { isPartialOrder = ≤-isPartialOrder
-  ; _≟_            = _≡?_
+  ; _≈?_           = _≡?_
   ; _≤?_           = _≤?_
   }
 
@@ -245,7 +245,7 @@ x ≈? y = toℕ x ℕ.≡? toℕ y
 ≈-isDecEquivalence : IsDecEquivalence _≈_
 ≈-isDecEquivalence = record
   { isEquivalence = ≈-isEquivalence
-  ; _≟_            = _≈?_
+  ; _≈?_           = _≈?_
   }
 ≈-decSetoid : DecSetoid _ _
 ≈-decSetoid = record

src/Data/Fin/Properties.agda

@@ -123,7 +123,7 @@ suc x ≡? suc y = map′ (cong suc) suc-injective (x ≡? y)
 ≡-isDecEquivalence : IsDecEquivalence {A = Fin n} _≡_
 ≡-isDecEquivalence = record
   { isEquivalence = ≡.isEquivalence
-  ; _≟_           = _≡?_
+  ; _≈?_          = _≡?_
   }
 
 ------------------------------------------------------------------------
@@ -356,7 +356,7 @@ m <? n = suc (toℕ m) ℕ.≤? toℕ n
 ≤-isDecTotalOrder : IsDecTotalOrder {A = Fin n} _≡_ _≤_
 ≤-isDecTotalOrder = record
   { isTotalOrder = ≤-isTotalOrder
-  ; _≟_          = _≡?_
+  ; _≈?_         = _≡?_
   ; _≤?_         = _≤?_
   }
 
@@ -1198,7 +1198,7 @@ module _ {ℓ} {S : Setoid a ℓ} (inj : Injection S (≡-setoid n)) where
   inj⇒decSetoid = record
     { isDecEquivalence = record
       { isEquivalence = isEquivalence
-      ; _≟_           = inj⇒≡?
+      ; _≈?_           = inj⇒≡?
       }
     }
 

src/Data/Fin/Subset/Properties.agda

@@ -317,7 +317,7 @@ module _ (n : ℕ) where
   ⊂-isDecStrictPartialOrder : IsDecStrictPartialOrder {A = Subset n} _≡_ _⊂_
   ⊂-isDecStrictPartialOrder = record
     { isStrictPartialOrder = ⊂-isStrictPartialOrder
-    ; _≟_  = ≡-dec _≡?_
+    ; _≈?_ = ≡-dec _≡?_
     ; _<?_ = _⊂?_
     }
 

src/Data/Float/Properties.agda

@@ -76,7 +76,7 @@ _≈?_ = On.decidable (Maybe.map Word64.toℕ ∘ toWord64) _≡_ (Maybe.≡-dec
 ≈-isDecEquivalence : IsDecEquivalence _≈_
 ≈-isDecEquivalence = record
   { isEquivalence = ≈-isEquivalence
-  ; _≟_           = _≈?_
+  ; _≈?_          = _≈?_
   }
 
 ≈-decSetoid : DecSetoid _ _

src/Data/Integer/Properties.agda

@@ -162,7 +162,7 @@ _≤?_ : Decidable _≤_
 ≤-isDecTotalOrder : IsDecTotalOrder _≡_ _≤_
 ≤-isDecTotalOrder = record
   { isTotalOrder = ≤-isTotalOrder
-  ; _≟_          = _≡?_
+  ; _≈?_         = _≡?_
   ; _≤?_         = _≤?_
   }
 
@@ -2404,4 +2404,3 @@ _≟_ = _≡?_
 "Warning: _≟_ was deprecated in v2.4.
 Please use _≡?_ instead."
 #-}
-

src/Data/List/Relation/Binary/Infix/Homogeneous/Properties.agda

@@ -42,6 +42,6 @@ isPartialOrder po = record
 isDecPartialOrder : IsDecPartialOrder R S → IsDecPartialOrder (Pointwise R) (Infix S)
 isDecPartialOrder dpo = record
   { isPartialOrder = isPartialOrder DPO.isPartialOrder
-  ; _≟_            = Pointwise.decidable DPO._≈?_
+  ; _≈?_           = Pointwise.decidable DPO._≈?_
   ; _≤?_           = infix? DPO._≤?_
   } where module DPO = IsDecPartialOrder dpo

src/Data/List/Relation/Binary/Lex/Strict.agda

@@ -203,7 +203,7 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} where
                           IsDecPartialOrder _≋_ _≤_
     ≤-isDecPartialOrder sto = record
       { isPartialOrder = ≤-isPartialOrder isStrictPartialOrder
-      ; _≟_             = Pointwise.decidable _≈?_
+      ; _≈?_            = Pointwise.decidable _≈?_
       ; _≤?_           = ≤-decidable _≈?_ _<?_
       } where open IsStrictTotalOrder sto
 
@@ -218,7 +218,7 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} where
                         IsDecTotalOrder _≋_ _≤_
     ≤-isDecTotalOrder sto = record
       { isTotalOrder = ≤-isTotalOrder sto
-      ; _≟_          = Pointwise.decidable _≈?_
+      ; _≈?_         = Pointwise.decidable _≈?_
       ; _≤?_         = ≤-decidable _≈?_ _<?_
       }
       where open IsStrictTotalOrder sto

src/Data/List/Relation/Binary/Pointwise.agda

@@ -65,7 +65,7 @@ isEquivalence eq = record
 isDecEquivalence : IsDecEquivalence R → IsDecEquivalence (Pointwise R)
 isDecEquivalence eq = record
   { isEquivalence = isEquivalence DE.isEquivalence
-  ; _≟_           = decidable     DE._≈?_
+  ; _≈?_          = decidable     DE._≈?_
   } where module DE = IsDecEquivalence eq
 
 isPreorder : IsPreorder R S → IsPreorder (Pointwise R) (Pointwise S)

src/Data/List/Relation/Binary/Prefix/Homogeneous/Properties.agda

@@ -43,6 +43,6 @@ isPartialOrder po = record
 isDecPartialOrder : IsDecPartialOrder R S → IsDecPartialOrder (Pointwise R) (Prefix S)
 isDecPartialOrder dpo = record
   { isPartialOrder = isPartialOrder DPO.isPartialOrder
-  ; _≟_            = Pointwise.decidable DPO._≈?_
+  ; _≈?_           = Pointwise.decidable DPO._≈?_
   ; _≤?_           = prefix? DPO._≤?_
   } where module DPO = IsDecPartialOrder dpo

src/Data/List/Relation/Binary/Sublist/DecPropositional.agda

@@ -35,7 +35,7 @@ open DecSetoidSublist (decSetoid _≈?_) using (_⊆?_) public
 ⊆-isDecPartialOrder : IsDecPartialOrder _≡_ _⊆_
 ⊆-isDecPartialOrder = record
   { isPartialOrder = ⊆-isPartialOrder
-  ; _≟_            = _≡?_
+  ; _≈?_           = _≡?_
   ; _≤?_           = _⊆?_
   }
 

src/Data/List/Relation/Binary/Sublist/DecSetoid.agda

@@ -41,7 +41,7 @@ _⊆?_ = HeterogeneousProperties.sublist? _≈?_
 ⊆-isDecPartialOrder : IsDecPartialOrder _≋_ _⊆_
 ⊆-isDecPartialOrder = record
   { isPartialOrder = ⊆-isPartialOrder
-  ; _≟_            = _≋?_
+  ; _≈?_           = _≋?_
   ; _≤?_           = _⊆?_
   }
 

src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda

@@ -448,7 +448,7 @@ module _ {E : Rel A e} {R : Rel A r} where
                       IsDecPartialOrder (Pointwise E) (Sublist R)
   isDecPartialOrder ER-isDecPartialOrder = record
     { isPartialOrder = isPartialOrder ER.isPartialOrder
-    ; _≟_            = Pw.decidable   ER._≈?_
+    ; _≈?_           = Pw.decidable   ER._≈?_
     ; _≤?_           = sublist?       ER._≤?_
     } where module ER = IsDecPartialOrder ER-isDecPartialOrder
 

src/Data/List/Relation/Binary/Suffix/Homogeneous/Properties.agda

@@ -42,6 +42,6 @@ isPartialOrder po = record
 isDecPartialOrder : IsDecPartialOrder R S → IsDecPartialOrder (Pointwise R) (Suffix S)
 isDecPartialOrder dpo = record
   { isPartialOrder = isPartialOrder DPO.isPartialOrder
-  ; _≟_             = Pointwise.decidable DPO._≈?_
+  ; _≈?_            = Pointwise.decidable DPO._≈?_
   ; _≤?_           = suffix? DPO._≤?_
   } where module DPO = IsDecPartialOrder dpo

src/Data/Maybe/Relation/Binary/Pointwise.agda

@@ -92,7 +92,7 @@ module _ {a r} {A : Set a} {R : Rel A r} where
   isDecEquivalence : IsDecEquivalence R → IsDecEquivalence (Pointwise R)
   isDecEquivalence R-isDecEquivalence = record
     { isEquivalence = isEquivalence R.isEquivalence
-    ; _≟_           = dec R._≈?_
+    ; _≈?_          = dec R._≈?_
     } where module R = IsDecEquivalence R-isDecEquivalence
 
   pointwise⊆any : ∀ {x} → Pointwise R (just x) ⊆ Any (R x)

src/Data/Nat/Binary/Properties.agda

@@ -584,7 +584,7 @@ x ≤? y with <-cmp x y
 ≤-isDecTotalOrder : IsDecTotalOrder _≡_ _≤_
 ≤-isDecTotalOrder = record
   { isTotalOrder = ≤-isTotalOrder
-  ; _≟_          = _≡?_
+  ; _≈?_         = _≡?_
   ; _≤?_         = _≤?_
   }
 

src/Data/Nat/Properties.agda

@@ -123,7 +123,7 @@ m ≡? n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n))
 ≡-isDecEquivalence : IsDecEquivalence (_≡_ {A = ℕ})
 ≡-isDecEquivalence = record
   { isEquivalence = isEquivalence
-  ; _≟_            = _≡?_
+  ; _≈?_           = _≡?_
   }
 
 ≡-decSetoid : DecSetoid 0ℓ 0ℓ
@@ -253,7 +253,7 @@ _≥?_ = flip _≤?_
 ≤-isDecTotalOrder : IsDecTotalOrder _≡_ _≤_
 ≤-isDecTotalOrder = record
   { isTotalOrder = ≤-isTotalOrder
-  ; _≟_          = _≡?_
+  ; _≈?_         = _≡?_
   ; _≤?_         = _≤?_
   }
 

src/Data/Product/Relation/Binary/Lex/NonStrict.agda

@@ -157,7 +157,7 @@ module _ {_≈₁_ : Rel A ℓ₁} {_≤₁_ : Rel A ℓ₂}
     { isTotalOrder = ×-isTotalOrder (_≟_ to₁)
                                     (isTotalOrder to₁)
                                     (isTotalOrder to₂)
-    ; _≟_          = Pointwise.×-decidable (_≈?_ to₁) (_≈?_ to₂)
+    ; _≈?_         = Pointwise.×-decidable (_≈?_ to₁) (_≈?_ to₂)
     ; _≤?_         = ×-decidable (_≈?_ to₁) (_≤?_ to₁) (_≤?_ to₂)
     }
     where open IsDecTotalOrder

src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda

@@ -108,7 +108,7 @@ Pointwise R S (a , c) (b , d) = (R a b) × (S c d)
 ×-isDecEquivalence eq₁ eq₂ = record
   { isEquivalence = ×-isEquivalence
                       (isEquivalence eq₁) (isEquivalence eq₂)
-  ; _≟_           = ×-decidable (_≈?_ eq₁) (_≈?_ eq₂)
+  ; _≈?_          = ×-decidable (_≈?_ eq₁) (_≈?_ eq₂)
   } where open IsDecEquivalence
 
 ×-isPreorder : IsPreorder ≈₁ R → IsPreorder ≈₂ S →

src/Data/Rational/Properties.agda

@@ -600,7 +600,7 @@ _≥?_ = flip _≤?_
 ≤-isDecTotalOrder : IsDecTotalOrder _≡_ _≤_
 ≤-isDecTotalOrder = record
   { isTotalOrder = ≤-isTotalOrder
-  ; _≟_          = _≡?_
+  ; _≈?_         = _≡?_
   ; _≤?_         = _≤?_
   }
 

src/Data/Rational/Unnormalised/Properties.agda

@@ -147,7 +147,7 @@ p ≃? q = Dec.map′ *≡* drop-*≡* (↥ p ℤ.* ↧ q ℤ.≡? ↥ q ℤ.* 
 ≃-isDecEquivalence : IsDecEquivalence _≃_
 ≃-isDecEquivalence = record
   { isEquivalence = ≃-isEquivalence
-  ; _≟_           = _≃?_
+  ; _≈?_          = _≃?_
   }
 
 ≄-isApartnessRelation : IsApartnessRelation _≃_ _≄_
@@ -326,7 +326,7 @@ _≥?_ = flip _≤?_
 ≤-isDecTotalOrder : IsDecTotalOrder _≃_ _≤_
 ≤-isDecTotalOrder = record
   { isTotalOrder = ≤-isTotalOrder
-  ; _≟_          = _≃?_
+  ; _≈?_         = _≃?_
   ; _≤?_         = _≤?_
   }
 

src/Data/String/Properties.agda

@@ -78,7 +78,7 @@ x ≈? y = Pointwise.decidable Char._≡?_ (toList x) (toList y)
 ≈-isDecEquivalence : IsDecEquivalence _≈_
 ≈-isDecEquivalence = record
   { isEquivalence = ≈-isEquivalence
-  ; _≟_           = _≈?_
+  ; _≈?_          = _≈?_
   }
 
 ≈-decSetoid : DecSetoid _ _

src/Data/Sum/Relation/Binary/LeftOrder.agda

@@ -203,7 +203,7 @@ module _ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂}
                         IsDecTotalOrder (Pointwise ≈₁ ≈₂) (∼₁ ⊎-< ∼₂)
   ⊎-<-isDecTotalOrder to₁ to₂ = record
     { isTotalOrder = ⊎-<-isTotalOrder (isTotalOrder to₁) (isTotalOrder to₂)
-    ; _≟_          = PW.⊎-decidable (_≈?_  to₁) (_≈?_  to₂)
+    ; _≈?_         = PW.⊎-decidable (_≈?_  to₁) (_≈?_  to₂)
     ; _≤?_         = ⊎-<-decidable (_≤?_ to₁) (_≤?_ to₂)
     }
     where open IsDecTotalOrder

src/Data/Sum/Relation/Binary/Pointwise.agda

@@ -142,7 +142,7 @@ drop-inj₂ (inj₂ x) = x
 ⊎-isDecEquivalence eq₁ eq₂ = record
   { isEquivalence =
       ⊎-isEquivalence (isEquivalence eq₁) (isEquivalence eq₂)
-  ; _≟_           = ⊎-decidable (_≈?_ eq₁) (_≈?_ eq₂)
+  ; _≈?_          = ⊎-decidable (_≈?_ eq₁) (_≈?_ eq₂)
   } where open IsDecEquivalence
 
 ⊎-isPreorder : IsPreorder ≈₁ R → IsPreorder ≈₂ S →

src/Data/Unit/Polymorphic/Properties.agda

@@ -81,7 +81,7 @@ _ ≡? _ = yes refl
 ≡-isDecTotalOrder : ∀ ℓ → IsDecTotalOrder {ℓ} _≡_ _≡_
 ≡-isDecTotalOrder ℓ = record
   { isTotalOrder = ≡-isTotalOrder ℓ
-  ; _≟_          = _≡?_
+  ; _≈?_         = _≡?_
   ; _≤?_         = _≡?_
   }
 

src/Data/Unit/Properties.agda

@@ -79,7 +79,7 @@ _ ≡? _ = yes refl
 ≡-isDecTotalOrder : IsDecTotalOrder _≡_ _≡_
 ≡-isDecTotalOrder = record
   { isTotalOrder = ≡-isTotalOrder
-  ; _≟_          = _≡?_
+  ; _≈?_         = _≡?_
   ; _≤?_         = _≡?_
   }
 
@@ -111,4 +111,3 @@ _≟_ = _≡?_
 "Warning: _≟_ was deprecated in v2.4.
 Please use _≡?_ instead."
 #-}
-

src/Data/Vec/Functional/Relation/Binary/Pointwise/Properties.agda

@@ -68,7 +68,7 @@ module _ {R : Rel A ℓ} where
                      ∀ n → IsDecEquivalence (Pointwise R {n})
   isDecEquivalence isDecEq n = record
     { isEquivalence = isEquivalence Eq.isEquivalence n
-    ; _≟_           = decidable Eq._≈?_
+    ; _≈?_          = decidable Eq._≈?_
     } where module Eq = IsDecEquivalence isDecEq
 
 ------------------------------------------------------------------------