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

doc/README/Data/List/Membership.agda

@@ -34,7 +34,7 @@ import Data.List.Membership.DecPropositional as DecPropMembership
 -- propositional equality over `ℕ` and it is also decidable. Therefore
 -- the module `DecPropMembership` should be opened as follows:
 
-open DecPropMembership ℕ._≟_
+open DecPropMembership ℕ._≡?_
 
 -- As membership is just an instance of `Any` we also need to import
 -- the constructors `here` and `there`. (See issue #553 on Github for
@@ -66,7 +66,7 @@ import Data.List.Membership.Propositional.Properties as PropProperties
 -- following the first `∈` refers to lists of type `List ℕ` whereas
 -- the second `∈` refers to lists of type `List Char`.
 
-open DecPropMembership Char._≟_ renaming (_∈_ to _∈ᶜ_)
+open DecPropMembership Char._≡?_ renaming (_∈_ to _∈ᶜ_)
 open SetoidProperties using (∈-map⁺)
 
 lem₂ : {v : ℕ} {xs : List ℕ} → v ∈ xs → fromℕ v ∈ᶜ map fromℕ xs

doc/README/Data/List/Relation/Binary/Subset.agda

@@ -22,10 +22,10 @@ module README.Data.List.Relation.Binary.Subset where
 
 -- Decidable equality over Strings
 open import Data.String.Base using (String)
-open import Data.String.Properties using (_≟_)
+open import Data.String.Properties using (_≡?_)
 
 -- Open the decidable membership module using Decidable ≡ over Strings
-open import Data.List.Membership.DecPropositional _≟_
+open import Data.List.Membership.DecPropositional _≡?_
 
 
 -- Simple cases are inductive proofs

doc/README/Data/Record.agda

@@ -21,7 +21,7 @@ import Data.Record as Record
 
 -- Let us use strings as labels.
 
-open Record String _≟_
+open Record String _≡?_
 
 -- Partial equivalence relations.
 

doc/README/Data/Trie/NonDependent.agda

@@ -83,7 +83,7 @@ record Lexer t : Set (suc t) where
 
   -- Two keywords are considered distinct if the strings are not equal
   Distinct : Rel Keyword 0ℓ
-  Distinct a b = ⌊ ¬? ((proj₁ a) String.≟ (proj₁ b)) ⌋
+  Distinct a b = ⌊ ¬? ((proj₁ a) String.≡? (proj₁ b)) ⌋
 
   field
 
@@ -175,7 +175,7 @@ module LetIn where
     LPAR RPAR : TOK
     ID : String → TOK
 
-  keywords : List# (String × TOK) (λ a b → ⌊ ¬? ((proj₁ a) String.≟ (proj₁ b)) ⌋)
+  keywords : List# (String × TOK) (λ a b → ⌊ ¬? ((proj₁ a) String.≡? (proj₁ b)) ⌋)
   keywords =  ("let" , LET)
            ∷# ("="   , EQ)
            ∷# ("in"  , IN)

doc/README/Foreign/Haskell.agda

@@ -92,12 +92,12 @@ main = run $ do
   content ← readFiniteFile "README/Foreign/Haskell.agda"
   let chars = toList content
   let cleanup = catMaybes ∘ List.map (λ c → if testChar c then just c else nothing)
-  let cleaned = dropWhile ('\n' ≟_) $ cleanup chars
+  let cleaned = dropWhile ('\n' ≡?_) $ cleanup chars
   case uncons cleaned of λ where
     nothing         → putStrLn "I cannot believe this file is filed with dashes only!"
     (just (c , cs)) → putStrLn $ unlines
                     $ ("First (non dash) character: " ++ Char.show c)
-                    ∷ ("Rest (dash free) of the line: " ++ fromList (takeWhile (¬? ∘ ('\n' ≟_)) cs))
+                    ∷ ("Rest (dash free) of the line: " ++ fromList (takeWhile (¬? ∘ ('\n' ≡?_)) cs))
                     ∷ []
 
 -- You can compile and run this test by writing:

doc/README/Function/Reasoning.agda

@@ -57,7 +57,7 @@ subpalindromes str = let Chars = List Char in
   |> filter (λ cs → 2 ≤? length cs)        ∶ List Chars
   -- only keep the ones that are palindromes
   |> map < fromList , fromList ∘ reverse > ∶ List (String × String)
-  |> filter (uncurry String._≟_)           ∶ List (String × String)
+  |> filter (uncurry String._≡?_)           ∶ List (String × String)
   |> map proj₁                             ∶ List String
 
 -- Test cases

doc/README/Nary.agda

@@ -338,14 +338,14 @@ exist₁ = 19 , 793 , 3059 , 10 , refl
 -- ∀[_] P = ∀ {a₁} → ⋯ → ∀ {aₙ} → P a₁ ⋯ aₙ
 
 all₁ : ∀[ (λ (a₁ a₂ : ℕ) → Dec (a₁ ≡ a₂)) ]
-all₁ {a₁} {a₂} = a₁ ≟ a₂
+all₁ {a₁} {a₂} = a₁ ≡? a₂
 
 ------------------------------------------------------------------------
 -- Π : (A₁ → ⋯ → Aₙ → Set r) → Set _
 -- Π P = ∀ a₁ → ⋯ → ∀ aₙ → P a₁ ⋯ aₙ
 
 all₂ : Π[ (λ (a₁ a₂ : ℕ) → Dec (a₁ ≡ a₂)) ]
-all₂ = _≟_
+all₂ = _≡?_
 
 ------------------------------------------------------------------------
 -- _⇒_ : (A₁ → ⋯ → Aₙ → Set r) → (A₁ → ⋯ → Aₙ → Set s) → (A₁ → ⋯ → Aₙ → Set _)

doc/style-guide.md

@@ -586,6 +586,12 @@ word within a compound word is capitalized except for the first word.
   converse relations are systematically introduced, eg `≥` as `\ge`
   and `≱` as `\gen`.
 
+* Decidable predicates and relations should typically be written as `R?`,
+  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`
+  - `_≈?_` 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/Algebra/Solver/CommutativeMonoid/Normal.agda

@@ -57,10 +57,10 @@ Normal n = Vec ℕ n
 
 -- We can decide if two normal forms are /syntactically/ equal.
 
-infix 5 _≟_
+infix 4 _≡?_
 
-_≟_ : DecidableEquality (Normal n)
-nf₁ ≟ nf₂ = Dec.map Pointwise-≡↔≡ (decidable ℕ._≟_ nf₁ nf₂)
+_≡?_ : DecidableEquality (Normal n)
+nf₁ ≡? nf₂ = Dec.map Pointwise-≡↔≡ (decidable ℕ._≡?_ nf₁ nf₂)
   where open Pointwise using (Pointwise-≡↔≡; decidable)
 
 ------------------------------------------------------------------------
@@ -162,3 +162,12 @@ sg-correct = singleton-correct
 "Warning: sg-correct was deprecated in v2.2.
 Please use singleton-correct instead."
 #-}
+
+-- Version 2.4
+
+infix 4 _≟_
+_≟_ = _≡?_
+{-# WARNING_ON_USAGE _≟_
+"Warning: _≟_ was deprecated in v2.4.
+Please use _≡?_ instead."
+#-}

src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda

@@ -56,10 +56,10 @@ Normal n = Vec Bool n
 
 -- We can decide if two normal forms are /syntactically/ equal.
 
-infix 5 _≟_
+infix 4 _≡?_
 
-_≟_ : DecidableEquality (Normal n)
-nf₁ ≟ nf₂ = Dec.map Pointwise-≡↔≡ (decidable Bool._≟_ nf₁ nf₂)
+_≡?_ : DecidableEquality (Normal n)
+nf₁ ≡? nf₂ = Dec.map Pointwise-≡↔≡ (decidable Bool._≡?_ nf₁ nf₂)
   where open Pointwise using (Pointwise-≡↔≡; decidable)
 
 ------------------------------------------------------------------------
@@ -167,3 +167,12 @@ sg-correct = singleton-correct
 "Warning: sg-correct was deprecated in v2.2.
 Please use singleton-correct instead."
 #-}
+
+-- Version 2.4
+
+infix 4 _≟_
+_≟_ = _≡?_
+{-# WARNING_ON_USAGE _≟_
+"Warning: _≟_ was deprecated in v2.4.
+Please use _≡?_ instead."
+#-}

src/Algebra/Solver/Monoid/Normal.agda

@@ -50,11 +50,11 @@ Normal n = List (Fin n)
 
 -- We can decide if two normal forms are /syntactically/ equal.
 
-infix 5 _≟_
+infix 4 _≡?_
 
-_≟_ : DecidableEquality (Normal n)
-nf₁ ≟ nf₂ = Dec.map′ ≋⇒≡ ≡⇒≋ (nf₁ ≋? nf₂)
-  where open ≋ Fin._≟_ using (_≋?_; ≋⇒≡; ≡⇒≋)
+_≡?_ : DecidableEquality (Normal n)
+nf₁ ≡? nf₂ = Dec.map′ ≋⇒≡ ≡⇒≋ (nf₁ ≋? nf₂)
+  where open ≋ Fin._≡?_ using (_≋?_; ≋⇒≡; ≡⇒≋)
 
 -- A normaliser.
 
@@ -87,3 +87,20 @@ correct (e₁ ⊕ e₂) ρ = begin
   ⟦ normalise e₁ ++ normalise e₂ ⟧⇓ ρ        ≈⟨ comp-correct (normalise e₁) (normalise e₂) ρ ⟩
   ⟦ normalise e₁ ⟧⇓ ρ ∙ ⟦ normalise e₂ ⟧⇓ ρ  ≈⟨ ∙-cong (correct e₁ ρ) (correct e₂ ρ) ⟩
   ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ                        ∎
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.4
+
+infix 4 _≟_
+
+_≟_ = _≡?_
+{-# WARNING_ON_USAGE _≟_
+"Warning: _≟_ was deprecated in v2.4.
+Please use _≡?_ instead."
+#-}

src/Algebra/Solver/Ring/NaturalCoefficients/Default.agda

@@ -18,7 +18,7 @@ module Algebra.Solver.Ring.NaturalCoefficients.Default
 
 import Algebra.Properties.Semiring.Mult as SemiringMultiplication using (_×_)
 open import Data.Maybe.Base using (Maybe; map)
-open import Data.Nat using (_≟_)
+open import Data.Nat using (_≡?_)
 open import Relation.Binary.Consequences using (dec⇒weaklyDec)
 import Relation.Binary.PropositionalEquality.Core as ≡ using (refl; cong)
 
@@ -27,6 +27,6 @@ open SemiringMultiplication semiring
 
 private
   dec : ∀ m n → Maybe (m × 1# ≈ n × 1#)
-  dec m n = map (λ { ≡.refl → refl }) (dec⇒weaklyDec _≟_ m n)
+  dec m n = map (λ { ≡.refl → refl }) (dec⇒weaklyDec _≡?_ m n)
 
 open import Algebra.Solver.Ring.NaturalCoefficients R dec public

src/Data/Bool.agda

@@ -17,4 +17,4 @@ open import Data.Bool.Base public
 -- Publicly re-export queries
 
 open import Data.Bool.Properties public
-  using (T?; _≟_; _≤?_; _<?_)
+  using (T?; _≟_; _≡?_; _≤?_; _<?_)

src/Data/Bool/Instances.agda

@@ -8,10 +8,10 @@
 
 module Data.Bool.Instances where
 
-open import Data.Bool.Properties using (_≟_; ≤-isDecTotalOrder)
+open import Data.Bool.Properties using (_≡?_; ≤-isDecTotalOrder)
 open import Relation.Binary.PropositionalEquality.Properties
   using (isDecEquivalence)
 
 instance
-  Bool-≡-isDecEquivalence = isDecEquivalence _≟_
+  Bool-≡-isDecEquivalence = isDecEquivalence _≡?_
   Bool-≤-isDecTotalOrder = ≤-isDecTotalOrder

src/Data/Bool/Properties.agda

@@ -59,19 +59,19 @@ private
 ------------------------------------------------------------------------
 -- Properties of _≡_
 
-infix 4 _≟_
+infix 4 _≡?_
 
-_≟_ : DecidableEquality Bool
-true  ≟ true  = yes refl
-false ≟ false = yes refl
-true  ≟ false = no λ()
-false ≟ true  = no λ()
+_≡?_ : DecidableEquality Bool
+true  ≡? true  = yes refl
+false ≡? false = yes refl
+true  ≡? false = no λ()
+false ≡? true  = no λ()
 
 ≡-setoid : Setoid 0ℓ 0ℓ
 ≡-setoid = setoid Bool
 
 ≡-decSetoid : DecSetoid 0ℓ 0ℓ
-≡-decSetoid = decSetoid _≟_
+≡-decSetoid = decSetoid _≡?_
 
 ------------------------------------------------------------------------
 -- Properties of _≤_
@@ -139,7 +139,7 @@ true  ≤? true  = yes b≤b
 ≤-isDecTotalOrder : IsDecTotalOrder _≡_ _≤_
 ≤-isDecTotalOrder = record
   { isTotalOrder = ≤-isTotalOrder
-  ; _≟_          = _≟_
+  ; _≈?_         = _≡?_
   ; _≤?_         = _≤?_
   }
 
@@ -884,3 +884,12 @@ push-function-into-if = if-float
 "Warning: push-function-into-if was deprecated in v2.0.
 Please use if-float instead."
 #-}
+
+-- Version 2.4
+
+infix 4 _≟_
+_≟_ = _≡?_
+{-# WARNING_ON_USAGE _≟_
+"Warning: _≟_ was deprecated in v2.4.
+Please use _≡?_ instead."
+#-}

src/Data/Bool/Solver.agda

@@ -13,18 +13,18 @@ module Data.Bool.Solver where
 import Algebra.Solver.Ring.Simple as Solver
 import Algebra.Solver.Ring.AlmostCommutativeRing as ACR
 open import Data.Bool.Properties
-  using (_≟_;  ∨-∧-commutativeSemiring; xor-∧-commutativeRing)
+  using (_≡?_;  ∨-∧-commutativeSemiring; xor-∧-commutativeRing)
 
 ------------------------------------------------------------------------
 -- A module for automatically solving propositional equivalences
 -- containing _∨_ and _∧_
 
 module ∨-∧-Solver =
-  Solver (ACR.fromCommutativeSemiring ∨-∧-commutativeSemiring) _≟_
+  Solver (ACR.fromCommutativeSemiring ∨-∧-commutativeSemiring) _≡?_
 
 ------------------------------------------------------------------------
 -- A module for automatically solving propositional equivalences
 -- containing _xor_ and _∧_
 
 module xor-∧-Solver =
-  Solver (ACR.fromCommutativeRing xor-∧-commutativeRing) _≟_
+  Solver (ACR.fromCommutativeRing xor-∧-commutativeRing) _≡?_

src/Data/Char.agda

@@ -13,4 +13,4 @@ module Data.Char where
 
 open import Data.Char.Base public
 open import Data.Char.Properties
-  using (_≈?_; _≟_; _<?_; _≤?_; _==_) public
+  using (_≈?_; _≟_; _≡?_; _<?_; _≤?_; _==_) public