[ fix ] Deprecate _==_ for 2.4

CHANGELOG.md

@@ -93,6 +93,11 @@ Deprecated names
   ε-comm  ↦   ε-central
   ```
 
+* In `Data.Char.Properties`:
+  ```agda
+  _==_ ↦ _≡ᵇ_
+  ```
+
 * In `Data.Fin.Properties`:
   ```agda
   ¬∀⟶∃¬-smallest  ↦   ¬∀⇒∃¬-smallest

src/Data/Char/Properties.agda

@@ -80,24 +80,24 @@ isDecEquivalence = ≡.isDecEquivalence _≟_
 ------------------------------------------------------------------------
 -- Boolean equality test.
 --
--- Why is the definition _==_ = primCharEquality not used? One reason
+-- Why is the definition _≡ᵇ_ = primCharEquality not used? One reason
 -- is that the present definition can sometimes improve type
 -- inference, at least with the version of Agda that is current at the
 -- time of writing: see unit-test below.
 
-infix 4 _==_
-_==_ : Char → Char → Bool
-c₁ == c₂ = isYes (c₁ ≟ c₂)
+infix 4 _≡ᵇ_
+_≡ᵇ_ : Char → Char → Bool
+c₁ ≡ᵇ c₂ = isYes (c₁ ≟ c₂)
 
 private
 
   -- The following unit test does not type-check (at the time of
   -- writing) if _==_ is replaced by primCharEquality.
 
   data P : (Char → Bool) → Set where
-    MkP : (c : Char) → P (c ==_)
+    MkP : (c : Char) → P (c ≡ᵇ_)
 
-  unit-test : P ('x' ==_)
+  unit-test : P ('x' ≡ᵇ_)
   unit-test = MkP _
 
 ------------------------------------------------------------------------
@@ -314,3 +314,12 @@ Please use <-strictPartialOrder instead."
 Please use <-strictTotalOrder instead."
 #-}
 
+
+-- Version 2.4
+
+_==_ : Char → Char → Bool
+_==_ = _≡ᵇ_
+{-# WARNING_ON_USAGE _==_
+"Warning: _==_ was deprecated in v2.4.
+Please use _≡ᵇ_ instead."
+#-}