From b06a7bbef3bb7311c53bd58617f6cf215b620605 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 9 Mar 2026 12:51:33 +0000
Subject: [PATCH 1/5] refactor: introduce revised notation, plus knock-ons

---
 CHANGELOG.md                                  | 34 ++++++++++++++
 .../List/Relation/Binary/Lex/NonStrict.agda   | 31 ++++++++++---
 src/Data/List/Relation/Binary/Lex/Strict.agda | 43 +++++++++++++-----
 .../Relation/Binary/Lex/NonStrict.agda        | 24 +++++++---
 .../Product/Relation/Binary/Lex/Strict.agda   | 19 +++++++-
 src/Data/String/Properties.agda               |  2 +-
 .../Vec/Relation/Binary/Lex/NonStrict.agda    | 29 ++++++++++--
 src/Data/Vec/Relation/Binary/Lex/Strict.agda  | 44 ++++++++++++++-----
 8 files changed, 186 insertions(+), 40 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2d61629e75..15991a643f 100644
--- a/CHANGELOG.md
+++ b/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     ↦   _∩?_
diff --git a/src/Data/List/Relation/Binary/Lex/NonStrict.agda b/src/Data/List/Relation/Binary/Lex/NonStrict.agda
index efd1520f82..f30c640f2d 100644
--- a/src/Data/List/Relation/Binary/Lex/NonStrict.agda
+++ b/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."
+#-}
diff --git a/src/Data/List/Relation/Binary/Lex/Strict.agda b/src/Data/List/Relation/Binary/Lex/Strict.agda
index 26f05b6878..586741fb07 100644
--- a/src/Data/List/Relation/Binary/Lex/Strict.agda
+++ b/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."
+#-}
diff --git a/src/Data/Product/Relation/Binary/Lex/NonStrict.agda b/src/Data/Product/Relation/Binary/Lex/NonStrict.agda
index 599a7d011c..3583836e90 100644
--- a/src/Data/Product/Relation/Binary/Lex/NonStrict.agda
+++ b/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."
+#-}
diff --git a/src/Data/Product/Relation/Binary/Lex/Strict.agda b/src/Data/Product/Relation/Binary/Lex/Strict.agda
index 7ccc8357f4..88876af13c 100644
--- a/src/Data/Product/Relation/Binary/Lex/Strict.agda
+++ b/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."
+#-}
diff --git a/src/Data/String/Properties.agda b/src/Data/String/Properties.agda
index 2728f47934..cb798c2262 100644
--- a/src/Data/String/Properties.agda
+++ b/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-≈ =
diff --git a/src/Data/Vec/Relation/Binary/Lex/NonStrict.agda b/src/Data/Vec/Relation/Binary/Lex/NonStrict.agda
index 24bee076ef..a51fec7b9e 100644
--- a/src/Data/Vec/Relation/Binary/Lex/NonStrict.agda
+++ b/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."
+#-}
diff --git a/src/Data/Vec/Relation/Binary/Lex/Strict.agda b/src/Data/Vec/Relation/Binary/Lex/Strict.agda
index b48244820c..e9a3609587 100644
--- a/src/Data/Vec/Relation/Binary/Lex/Strict.agda
+++ b/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."
+#-}

From e0edba7c2d99c77095453c961e46c0108724fabb Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 10 Mar 2026 08:33:09 +0000
Subject: [PATCH 2/5] refactor: use `variable`s

---
 src/Data/List/Relation/Binary/Lex.agda        | 29 +++++++++++--------
 .../List/Relation/Binary/Lex/NonStrict.agda   |  2 +-
 2 files changed, 18 insertions(+), 13 deletions(-)

diff --git a/src/Data/List/Relation/Binary/Lex.agda b/src/Data/List/Relation/Binary/Lex.agda
index 1baaf2a4a0..fe4fdde580 100644
--- a/src/Data/List/Relation/Binary/Lex.agda
+++ b/src/Data/List/Relation/Binary/Lex.agda
@@ -16,7 +16,7 @@ open import Data.List.Relation.Binary.Pointwise.Base
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
 open import Function.Base using (_∘_; flip; id)
 open import Function.Bundles using (_⇔_; mk⇔)
-open import Level using (_⊔_)
+open import Level using (Level; _⊔_)
 open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Nullary.Decidable as Dec
   using (Dec; yes; no; _×?_; _⊎?_)
@@ -26,6 +26,14 @@ open import Relation.Binary.Definitions
   using (Symmetric; Transitive; Irreflexive; Asymmetric; Antisymmetric
         ; Decidable; _Respects₂_; _Respects_)
 
+private
+  variable
+    a ℓ₁ ℓ₂ : Level
+    A : Set a
+    x y : A
+    xs ys : List A
+    
+
 
 ------------------------------------------------------------------------
 -- Re-exporting the core definitions and properties
@@ -35,20 +43,17 @@ open import Data.List.Relation.Binary.Lex.Core public
 ------------------------------------------------------------------------
 -- Properties
 
-module _ {a ℓ₁ ℓ₂} {A : Set a} {P : Set}
-         {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where
+module _ {A : Set a} {P : Set} {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where
 
   private
     _≋_ = Pointwise _≈_
     _<_ = Lex P _≈_ _≺_
 
-  ¬≤-this : ∀ {x y xs ys} → ¬ (x ≈ y) → ¬ (x ≺ y) →
-            ¬ (x ∷ xs) < (y ∷ ys)
+  ¬≤-this : ¬ (x ≈ y) → ¬ (x ≺ y) → ¬ (x ∷ xs) < (y ∷ ys)
   ¬≤-this x≉y x≮y (this x≺y)       = x≮y x≺y
   ¬≤-this x≉y x≮y (next x≈y xs<ys) = x≉y x≈y
 
-  ¬≤-next : ∀ {x y xs ys} → ¬ x ≺ y → ¬ xs < ys →
-            ¬ (x ∷ xs) < (y ∷ ys)
+  ¬≤-next : ¬ x ≺ y → ¬ xs < ys → ¬ (x ∷ xs) < (y ∷ ys)
   ¬≤-next x≮y xs≮ys (this x≺y)     = x≮y x≺y
   ¬≤-next x≮y xs≮ys (next _ xs<ys) = xs≮ys xs<ys
 
@@ -63,7 +68,7 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} {P : Set}
     as (next x≈y xs<ys) (this y≺x)       = contradiction y≺x (ir (sym x≈y))
     as (next x≈y xs<ys) (next y≈x ys<xs) = x≈y ∷ as xs<ys ys<xs
 
-  toSum : ∀ {x y xs ys} → (x ∷ xs) < (y ∷ ys) → (x ≺ y ⊎ (x ≈ y × xs < ys))
+  toSum : (x ∷ xs) < (y ∷ ys) → x ≺ y ⊎ (x ≈ y × xs < ys)
   toSum (this x≺y) = inj₁ x≺y
   toSum (next x≈y xs<ys) = inj₂ (x≈y , xs<ys)
 
@@ -87,14 +92,14 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} {P : Set}
   respects₂ eq (resp₁ , resp₂) = resp¹ , resp²
     where
     open IsEquivalence eq using (sym; trans)
-    resp¹ : ∀ {xs} → Lex P _≈_ _≺_ xs Respects _≋_
+    resp¹ : Lex P _≈_ _≺_ xs Respects _≋_
     resp¹ []            xs<[]            = xs<[]
     resp¹ (_   ∷ _)     halt             = halt
     resp¹ (x≈y ∷ _)     (this z≺x)       = this (resp₁ x≈y z≺x)
     resp¹ (x≈y ∷ xs≋ys) (next z≈x zs<xs) =
       next (trans z≈x x≈y) (resp¹ xs≋ys zs<xs)
 
-    resp² : ∀ {ys} → flip (Lex P _≈_ _≺_) ys Respects _≋_
+    resp² : flip (Lex P _≈_ _≺_) ys Respects _≋_
     resp² []            []<ys            = []<ys
     resp² (x≈z ∷ _)     (this x≺y)       = this (resp₂ x≈z x≺y)
     resp² (x≈z ∷ xs≋zs) (next x≈y xs<ys) =
@@ -102,10 +107,10 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} {P : Set}
 
 
   []<[]-⇔ : P ⇔ [] < []
-  []<[]-⇔ = mk⇔ base (λ { (base p) → p })
+  []<[]-⇔ = mk⇔ base λ { (base p) → p }
 
 
-  ∷<∷-⇔ : ∀ {x y xs ys} → (x ≺ y ⊎ (x ≈ y × xs < ys)) ⇔ (x ∷ xs) < (y ∷ ys)
+  ∷<∷-⇔ : (x ≺ y ⊎ (x ≈ y × xs < ys)) ⇔ (x ∷ xs) < (y ∷ ys)
   ∷<∷-⇔ = mk⇔ [ this , uncurry next ] toSum
 
   module _ (dec-P : Dec P) (dec-≈ : Decidable _≈_) (dec-≺ : Decidable _≺_)
diff --git a/src/Data/List/Relation/Binary/Lex/NonStrict.agda b/src/Data/List/Relation/Binary/Lex/NonStrict.agda
index f30c640f2d..ff04641669 100644
--- a/src/Data/List/Relation/Binary/Lex/NonStrict.agda
+++ b/src/Data/List/Relation/Binary/Lex/NonStrict.agda
@@ -19,7 +19,7 @@ open import Function.Base using (const; id)
 import Data.List.Relation.Binary.Lex.Strict as Strict
 open import Level using (Level; _⊔_)
 open import Relation.Nullary.Negation.Core using (¬_)
-open import Relation.Nullary using (yes; no)
+open import Relation.Nullary.Decidable.Core using (yes; no)
 open import Relation.Binary.Core using (Rel; _⇒_)
 open import Relation.Binary.Bundles
 open import Relation.Binary.Structures

From affaa2fcb13187c380609dd8518289b5ced3fa9e Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 17 Mar 2026 09:19:38 +0000
Subject: [PATCH 3/5] fix: typo

---
 CHANGELOG.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 028a78f717..faea9f24d5 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -113,7 +113,7 @@ Deprecated names
 
 * In `Data.Product.Relation.Binary.Lex.NonStrict`:
   ```agda
-  ×-decidable    ↦   <ₗₑₓ?
+  ×-decidable    ↦   ≤ₗₑₓ?
   ```
 
 * In `Data.Product.Relation.Binary.Lex.Strict`:

From 059f5c988e3bf11a201233dd42b5c9a8a0e89f30 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 17 Mar 2026 09:24:26 +0000
Subject: [PATCH 4/5] fix: typo

---
 src/Data/Product/Relation/Binary/Lex/NonStrict.agda | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/Data/Product/Relation/Binary/Lex/NonStrict.agda b/src/Data/Product/Relation/Binary/Lex/NonStrict.agda
index 3583836e90..873cc344b9 100644
--- a/src/Data/Product/Relation/Binary/Lex/NonStrict.agda
+++ b/src/Data/Product/Relation/Binary/Lex/NonStrict.agda
@@ -82,9 +82,9 @@ 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 _≤ₗₑₓ_
-  <ₗₑₓ? ≈?₁ ≤?₁ ≤?₂ =
+  ≤ₗₑₓ? ≈?₁ ≤?₁ ≤?₂ =
     Strict.<ₗₑₓ? ≈?₁ (Conv.<-decidable _ _ ≈?₁ ≤?₁) ≤?₂
 
 module _ {_≈₁_ : Rel A ℓ₁} {_≤₁_ : Rel A ℓ₂}
@@ -157,7 +157,7 @@ module _ {_≈₁_ : Rel A ℓ₁} {_≤₁_ : Rel A ℓ₂}
                                     (isTotalOrder to₁)
                                     (isTotalOrder to₂)
     ; _≟_          = Pointwise.×-decidable (_≟_ to₁) (_≟_ to₂)
-    ; _≤?_         = <ₗₑₓ? (_≟_ to₁) (_≤?_ to₁) (_≤?_ to₂)
+    ; _≤?_         = ≤ₗₑₓ? (_≟_ to₁) (_≤?_ to₁) (_≤?_ to₂)
     }
     where open IsDecTotalOrder
 
@@ -192,8 +192,8 @@ module _ {_≈₁_ : Rel A ℓ₁} {_≤₁_ : Rel A ℓ₂}
 
 -- Version 2.4
 
-×-decidable = <ₗₑₓ?
+×-decidable = ≤ₗₑₓ?
 {-# WARNING_ON_USAGE ×-decidable
 "Warning: ×-decidable was deprecated in v2.4.
-Please use <ₗₑₓ? instead."
+Please use ≤ₗₑₓ? instead."
 #-}

From 09327cd699d998059e039928eec9bc969fb36991 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 17 Mar 2026 09:26:13 +0000
Subject: [PATCH 5/5] fix: whitespace

---
 src/Data/List/Relation/Binary/Lex.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/List/Relation/Binary/Lex.agda b/src/Data/List/Relation/Binary/Lex.agda
index fe4fdde580..979fb6e4c0 100644
--- a/src/Data/List/Relation/Binary/Lex.agda
+++ b/src/Data/List/Relation/Binary/Lex.agda
@@ -32,7 +32,7 @@ private
     A : Set a
     x y : A
     xs ys : List A
-    
+
 
 
 ------------------------------------------------------------------------