[ refactor ] introduce revised notation for decidability of Lexicographic orderings, plus knock-ons

CHANGELOG.md

@@ -89,6 +89,28 @@ Deprecated names
   ¬∀⟶∃¬-          ↦   ¬∀⇒∃¬
   ```
 
+* In `Data.List.Relation.Binary.Lex.NonStrict`:
+  ```agda
+  <-decidable    ↦   _<?_
+  ≤-decidable    ↦   _≤?_
+  ```
+
+* In `Data.List.Relation.Binary.Lex.Strict`:
+  ```agda
+  <-decidable    ↦   _<?_
+  ≤-decidable    ↦   _≤?_
+  ```
+
+* In `Data.Product.Relation.Binary.Lex.NonStrict`:
+  ```agda
+  ×-decidable    ↦   <ₗₑₓ?
+  ```
+
+* In `Data.Product.Relation.Binary.Lex.Strict`:
+  ```agda
+  ×-decidable    ↦   <ₗₑₓ?
+  ```
+
 * In `Data.Rational.Properties`:
   ```agda
   nonPos*nonPos⇒nonPos  ↦  nonPos*nonPos⇒nonNeg
@@ -99,6 +121,18 @@ Deprecated names
   truncate-irrelevant  ↦  Relation.Binary.PropositionalEquality.Core.refl
   ```
 
+* In `Data.Vec.Relation.Binary.Lex.NonStrict`:
+  ```agda
+  <-decidable    ↦   _<?_
+  ≤-decidable    ↦   _≤?_
+  ```
+
+* In `Data.Vec.Relation.Binary.Lex.Strict`:
+  ```agda
+  <-decidable    ↦   _<?_
+  ≤-decidable    ↦   _≤?_
+  ```
+
 * In `Relation.Binary.Construct.Intersection`:
   ```agda
   decidable     ↦   _∩?_

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

@@ -86,8 +86,8 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} where
     <-compare sym _≟_ antisym tot =
       Strict.<-compare sym (Conv.<-trichotomous _ _ sym _≟_ antisym tot)
 
-    <-decidable : Decidable _≈_ → Decidable _≼_ → Decidable _<_
-    <-decidable _≟_ _≼?_ =
+    _<?_ : Decidable _≈_ → Decidable _≼_ → Decidable _<_
+    _<?_ _≟_ _≼?_ =
       Core.decidable (no id) _≟_ (Conv.<-decidable _ _ _≟_ _≼?_)
 
     <-isStrictPartialOrder : IsPartialOrder _≈_ _≼_ →
@@ -149,9 +149,9 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} where
     ≤-resp₂ : IsEquivalence _≈_ → _≼_ Respects₂ _≈_ → _≤_ Respects₂ _≋_
     ≤-resp₂ eq resp = Core.respects₂ eq (Conv.<-resp-≈ _ _ eq resp)
 
-    ≤-decidable : Decidable _≈_ → Decidable _≼_ → Decidable _≤_
-    ≤-decidable _≟_ _≼?_ =
-      Core.decidable (yes tt) _≟_ (Conv.<-decidable _ _ _≟_ _≼?_)
+    _≤?_ : Decidable _≈_ → Decidable _≼_ → Decidable _≤_
+    _≤?_ _≟_ _≼?_ =
+      Core.decidable (yes _) _≟_ (Conv.<-decidable _ _ _≟_ _≼?_)
 
     ≤-total : Symmetric _≈_ → Decidable _≈_ → Antisymmetric _≈_ _≼_ →
               Total _≼_ → Total _≤_
@@ -197,3 +197,24 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} where
 ≤-decTotalOrder dtot = record
   { isDecTotalOrder = ≤-isDecTotalOrder isDecTotalOrder
   } where open DecTotalOrder dtot
+
+
+------------------------------------------------------------------------
+-- 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."
+#-}
+
+≤-decidable = _≤?_
+{-# WARNING_ON_USAGE ≤-decidable
+"Warning: ≤-decidable was deprecated in v2.4.
+Please use _≤?_ instead."
+#-}

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

@@ -100,8 +100,8 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} where
     ...   | tri> xs≮ys xs≉ys ys<xs =
             tri> (¬≤-next x≮y xs≮ys) (xs≉ys ∘ tail) (next (sym x≈y) ys<xs)
 
-    <-decidable : Decidable _≈_ → Decidable _≺_ → Decidable _<_
-    <-decidable = Core.decidable (no id)
+    _<?_ : Decidable _≈_ → Decidable _≺_ → Decidable _<_
+    _<?_ = Core.decidable (no id)
 
     <-respects₂ : IsEquivalence _≈_ → _≺_ Respects₂ _≈_ →
                   _<_ Respects₂ _≋_
@@ -176,8 +176,8 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} where
     ...   | inj₁ xs≲ys = inj₁ (next      x≈y  xs≲ys)
     ...   | inj₂ ys≲xs = inj₂ (next (sym x≈y) ys≲xs)
 
-    ≤-decidable : Decidable _≈_ → Decidable _≺_ → Decidable _≤_
-    ≤-decidable = Core.decidable (yes _)
+    _≤?_ : Decidable _≈_ → Decidable _≺_ → Decidable _≤_
+    _≤?_ = Core.decidable (yes _)
 
     ≤-respects₂ : IsEquivalence _≈_ → _≺_ Respects₂ _≈_ →
                   _≤_ Respects₂ _≋_
@@ -202,10 +202,10 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} where
     ≤-isDecPartialOrder : IsStrictTotalOrder _≈_ _≺_ →
                           IsDecPartialOrder _≋_ _≤_
     ≤-isDecPartialOrder sto = record
-      { isPartialOrder = ≤-isPartialOrder isStrictPartialOrder
-      ; _≟_            = Pointwise.decidable _≟_
-      ; _≤?_           = ≤-decidable _≟_ _<?_
-      } where open IsStrictTotalOrder sto
+      { isPartialOrder = ≤-isPartialOrder O.isStrictPartialOrder
+      ; _≟_            = Pointwise.decidable O._≟_
+      ; _≤?_           = O._≟_ ≤?  O._<?_
+      } where module O = IsStrictTotalOrder sto
 
     ≤-isTotalOrder : IsStrictTotalOrder _≈_ _≺_ → IsTotalOrder _≋_ _≤_
     ≤-isTotalOrder sto = record
@@ -218,10 +218,10 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} where
                         IsDecTotalOrder _≋_ _≤_
     ≤-isDecTotalOrder sto = record
       { isTotalOrder = ≤-isTotalOrder sto
-      ; _≟_          = Pointwise.decidable _≟_
-      ; _≤?_         = ≤-decidable _≟_ _<?_
+      ; _≟_          = Pointwise.decidable O._≟_
+      ; _≤?_         = O._≟_ ≤?  O._<?_
       }
-      where open IsStrictTotalOrder sto
+      where module O = IsStrictTotalOrder sto
 
 ≤-preorder : ∀ {a ℓ₁ ℓ₂} → Preorder a ℓ₁ ℓ₂ → Preorder _ _ _
 ≤-preorder pre = record
@@ -245,3 +245,24 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} where
 ≤-decTotalOrder sto = record
   { isDecTotalOrder = ≤-isDecTotalOrder isStrictTotalOrder
   } where open StrictTotalOrder sto
+
+
+------------------------------------------------------------------------
+-- 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."
+#-}
+
+≤-decidable = _≤?_
+{-# WARNING_ON_USAGE ≤-decidable
+"Warning: ≤-decidable was deprecated in v2.4.
+Please use _≤?_ instead."
+#-}

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

@@ -82,11 +82,10 @@ module _ {_≈₁_ : Rel A ℓ₁} {_≤₁_ : Rel A ℓ₂} {_≤₂_ : Rel B 
     ...   | inj₁ x₂≤y₂ = inj₁ (inj₂ (x₁≈y₁ , x₂≤y₂))
     ...   | inj₂ x₂≥y₂ = inj₂ (inj₂ (sym₁ x₁≈y₁ , x₂≥y₂))
 
-  ×-decidable : Decidable _≈₁_ → Decidable _≤₁_ → Decidable _≤₂_ →
+  <ₗₑₓ? : Decidable _≈₁_ → Decidable _≤₁_ → Decidable _≤₂_ →
                 Decidable _≤ₗₑₓ_
-  ×-decidable dec-≈₁ dec-≤₁ dec-≤₂ =
-    Strict.×-decidable dec-≈₁ (Conv.<-decidable _ _ dec-≈₁ dec-≤₁)
-                       dec-≤₂
+  <ₗₑₓ? ≈?₁ ≤?₁ ≤?₂ =
+    Strict.<ₗₑₓ? ≈?₁ (Conv.<-decidable _ _ ≈?₁ ≤?₁) ≤?₂
 
 module _ {_≈₁_ : Rel A ℓ₁} {_≤₁_ : Rel A ℓ₂}
          {_≈₂_ : Rel B ℓ₃} {_≤₂_ : Rel B ℓ₄}
@@ -158,7 +157,7 @@ module _ {_≈₁_ : Rel A ℓ₁} {_≤₁_ : Rel A ℓ₂}
                                     (isTotalOrder to₁)
                                     (isTotalOrder to₂)
     ; _≟_          = Pointwise.×-decidable (_≟_ to₁) (_≟_ to₂)
-    ; _≤?_         = ×-decidable (_≟_ to₁) (_≤?_ to₁) (_≤?_ to₂)
+    ; _≤?_         = <ₗₑₓ? (_≟_ to₁) (_≤?_ to₁) (_≤?_ to₂)
     }
     where open IsDecTotalOrder
 
@@ -183,3 +182,18 @@ module _ {_≈₁_ : Rel A ℓ₁} {_≤₁_ : Rel A ℓ₂}
 ×-decTotalOrder t₁ t₂ = record
   { isDecTotalOrder = ×-isDecTotalOrder O₁.isDecTotalOrder O₂.isDecTotalOrder
   } where module O₁ = DecTotalOrder t₁; module O₂ = DecTotalOrder t₂
+
+
+------------------------------------------------------------------------
+-- 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."
+#-}

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

@@ -107,9 +107,9 @@ module _ {_≈₁_ : Rel A ℓ₁} {_<₁_ : Rel A ℓ₂} {_<₂_ : Rel B ℓ
   ...   | inj₁ x₂≤y₂ = inj₁ (inj₂ (x₁≈y₁     , x₂≤y₂))
   ...   | inj₂ y₂≤x₂ = inj₂ (inj₂ (sym x₁≈y₁ , y₂≤x₂))
 
-  ×-decidable : Decidable _≈₁_ → Decidable _<₁_ → Decidable _<₂_ →
+  <ₗₑₓ? : Decidable _≈₁_ → Decidable _<₁_ → Decidable _<₂_ →
                 Decidable _<ₗₑₓ_
-  ×-decidable _≈₁?_ _<₁?_ _<₂?_ x y =
+  <ₗₑₓ? _≈₁?_ _<₁?_ _<₂?_ x y =
     proj₁ x <₁? proj₁ y
       ⊎?
     (proj₁ x ≈₁? proj₁ y
@@ -304,3 +304,18 @@ module _ {_≈₁_ : Rel A ℓ₁} {_<₁_ : Rel A ℓ₂}
   { isStrictTotalOrder = ×-isStrictTotalOrder
       (isStrictTotalOrder s₁) (isStrictTotalOrder s₂)
   } where open StrictTotalOrder
+
+
+------------------------------------------------------------------------
+-- 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."
+#-}

src/Data/String/Properties.agda

@@ -105,7 +105,7 @@ x ≟ y = map′ ≈⇒≡ ≈-reflexive $ x ≈? y
 
 infix 4 _<?_
 _<?_ : Decidable _<_
-x <? y = StrictLex.<-decidable Char._≟_ Char._<?_ (toList x) (toList y)
+x <? y = StrictLex._<?_ Char._≟_ Char._<?_ (toList x) (toList y)
 
 <-isStrictPartialOrder-≈ : IsStrictPartialOrder _≈_ _<_
 <-isStrictPartialOrder-≈ =

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

@@ -103,8 +103,8 @@ module _ {_≈_ : Rel A ℓ₁} {_≼_ : Rel A ℓ₂} where
   <-cmp ≈-sym _≟_ ≼-antisym ≼-total = Strict.<-cmp ≈-sym
     (Conv.<-trichotomous _ _ ≈-sym _≟_ ≼-antisym ≼-total)
 
-  <-dec : Decidable _≈_ → Decidable _≼_ → ∀ {m n} → Decidable (_<_ {m} {n})
-  <-dec _≟_ _≼?_ = Core.decidable (no id) _≟_
+  _<?_ : Decidable _≈_ → Decidable _≼_ → ∀ {m n} → Decidable (_<_ {m} {n})
+  _<?_ _≟_ _≼?_ = Core.decidable (no id) _≟_
     (Conv.<-decidable _ _ _≟_ _≼?_)
 
 ------------------------------------------------------------------------
@@ -189,9 +189,9 @@ module _ {_≈_ : Rel A ℓ₁} {_≼_ : Rel A ℓ₂} where
   ≤-total ≈-sym _≟_ ≼-antisym ≼-total = Strict.≤-total ≈-sym
     (Conv.<-trichotomous _ _ ≈-sym _≟_ ≼-antisym ≼-total)
 
-  ≤-dec : Decidable _≈_ → Decidable _≼_ →
+  _≤?_ : Decidable _≈_ → Decidable _≼_ →
           ∀ {m n} → Decidable (_≤_ {m} {n})
-  ≤-dec _≟_ _≼?_ = Core.decidable (yes tt) _≟_
+  _≤?_ _≟_ _≼?_ = Core.decidable (yes tt) _≟_
     (Conv.<-decidable _ _ _≟_ _≼?_)
 
   ≤-resp₂ : IsEquivalence _≈_ → _≼_ Respects₂ _≈_ →
@@ -272,3 +272,24 @@ module ≤-Reasoning  {_≈_ : Rel A ℓ₁} {_≼_ : Rel A ℓ₂}
     (<-transˡ ≼-po)
     (<-transʳ ≼-po)
     public
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.4
+
+<-dec = _<?_
+{-# WARNING_ON_USAGE <-dec
+"Warning: <-dec was deprecated in v2.4.
+Please use _<?_ instead."
+#-}
+
+≤-dec = _≤?_
+{-# WARNING_ON_USAGE ≤-dec
+"Warning: ≤-dec was deprecated in v2.4.
+Please use _≤?_ instead."
+#-}

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

@@ -116,9 +116,9 @@ module _ {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where
     ...   | tri≈ xs≮ys xs≋ys xs≯ys = tri≈ (≰-next x⊀y xs≮ys) (x≈y ∷ xs≋ys) (≰-next x⊁y xs≯ys)
     ...   | tri> xs≮ys xs≋̸ys xs>ys = tri> (≰-next x⊀y xs≮ys) (xs≋̸ys ∘ tail) (next (≈-sym x≈y) xs>ys)
 
-  <-decidable : Decidable _≈_ → Decidable _≺_ →
+  _<?_ : Decidable _≈_ → Decidable _≺_ →
                 ∀ {m n} → Decidable (_<_ {m} {n})
-  <-decidable = Core.decidable (no id)
+  _<?_ = Core.decidable (no id)
 
   <-respectsˡ : IsPartialEquivalence _≈_ → _≺_ Respectsˡ _≈_ →
                 ∀ {m n} → _Respectsˡ_ (_<_ {m} {n}) _≋_
@@ -168,7 +168,7 @@ module _ {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where
   <-isDecStrictPartialOrder ≺-isDecStrictPartialOrder = record
     { isStrictPartialOrder = <-isStrictPartialOrder O.isStrictPartialOrder
     ; _≟_                  = Pointwise.decidable O._≟_
-    ; _<?_                 = <-decidable O._≟_ O._<?_
+    ; _<?_                 = O._≟_ <? O._<?_
     } where module O = IsDecStrictPartialOrder ≺-isDecStrictPartialOrder
 
   <-isStrictTotalOrder : IsStrictTotalOrder _≈_ _≺_ →
@@ -249,9 +249,9 @@ module _ {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where
     ...   | inj₁ xs<ys = inj₁ (next x≈y xs<ys)
     ...   | inj₂ xs>ys = inj₂ (next (≈-sym x≈y) xs>ys)
 
-  ≤-dec : Decidable _≈_ → Decidable _≺_ →
+  _≤?_ : Decidable _≈_ → Decidable _≺_ →
           ∀ {m n} → Decidable (_≤_ {m} {n})
-  ≤-dec = Core.decidable (yes tt)
+  _≤?_ = Core.decidable (yes tt)
 
   ≤-irrelevant : Irrelevant _≈_ → Irrelevant _≺_ → Irreflexive _≈_ _≺_ →
                  ∀ {m n} → Irrelevant (_≤_ {m} {n})
@@ -278,10 +278,10 @@ module _ {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where
   ≤-isDecPartialOrder : IsDecStrictPartialOrder _≈_ _≺_ →
                         ∀ {n} → IsDecPartialOrder (_≋_ {n} {n}) _≤_
   ≤-isDecPartialOrder ≺-isDecStrictPartialOrder = record
-    { isPartialOrder = ≤-isPartialOrder isStrictPartialOrder
-    ; _≟_            = Pointwise.decidable _≟_
-    ; _≤?_           = ≤-dec _≟_ _<?_
-    } where open IsDecStrictPartialOrder ≺-isDecStrictPartialOrder
+    { isPartialOrder = ≤-isPartialOrder O.isStrictPartialOrder
+    ; _≟_            = Pointwise.decidable O._≟_
+    ; _≤?_           = O._≟_ ≤? O._<?_
+    } where module O = IsDecStrictPartialOrder ≺-isDecStrictPartialOrder
 
   ≤-isTotalOrder : IsStrictTotalOrder _≈_ _≺_ →
                    ∀ {n} → IsTotalOrder (_≋_ {n} {n}) _≤_
@@ -294,9 +294,9 @@ module _ {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where
                       ∀ {n} → IsDecTotalOrder (_≋_ {n} {n}) _≤_
   ≤-isDecTotalOrder ≺-isStrictTotalOrder = record
     { isTotalOrder = ≤-isTotalOrder ≺-isStrictTotalOrder
-    ; _≟_          = Pointwise.decidable _≟_
-    ; _≤?_         = ≤-dec _≟_ _<?_
-    } where open IsStrictTotalOrder ≺-isStrictTotalOrder
+    ; _≟_          = Pointwise.decidable O._≟_
+    ; _≤?_         = O._≟_ ≤? O._<?_
+    } where module O = IsStrictTotalOrder ≺-isStrictTotalOrder
 
 ------------------------------------------------------------------------
 -- Bundles
@@ -348,3 +348,23 @@ module ≤-Reasoning
     (<-transʳ Eq.isPartialEquivalence <-resp-≈ trans)
     public
 
+
+------------------------------------------------------------------------
+-- 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."
+#-}
+
+≤-decidable = _≤?_
+{-# WARNING_ON_USAGE ≤-decidable
+"Warning: ≤-decidable was deprecated in v2.4.
+Please use _≤?_ instead."
+#-}