Making (more) arguments implicit in lexicographic ordering lemmas

Author: jamesmckinna

CHANGELOG.md

@@ -784,6 +784,9 @@ Non-backwards compatible changes
   properties about the orderings themselves the second index must be provided
   explicitly.
 
+* The argument `xs` in `xs≮[]` in `Data.{List|Vec}.Relation.Binary.Lex.Strict`
+  introduced in PRs #1648 and #1672 has now been made implicit.
+
 * Issue #2075 (Johannes Waldmann): wellfoundedness of the lexicographic ordering
   on products, defined in `Data.Product.Relation.Binary.Lex.Strict`, no longer
   requires the assumption of symmetry for the first equality relation `_≈₁_`,
@@ -2705,7 +2708,7 @@ Other minor changes
 
 * Added new proofs in `Data.Vec.Relation.Binary.Lex.Strict`:
   ```agda
-  xs≮[] : ∀ {n} (xs : Vec A n) → ¬ xs < []
+  xs≮[] : {xs : Vec A n} → ¬ xs < []
   <-respectsˡ : IsPartialEquivalence _≈_ → _≺_ Respectsˡ _≈_ →
                 ∀ {m n} → _Respectsˡ_ (_<_ {m} {n}) _≋_
   <-respectsʳ : IsPartialEquivalence _≈_ → _≺_ Respectsʳ _≈_ →

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

@@ -51,11 +51,11 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} where
       _≋_ = Pointwise _≈_
       _<_ = Lex-< _≈_ _≺_
 
-    xs≮[] : ∀ xs → ¬ xs < []
-    xs≮[] _ (base ())
+    xs≮[] : ∀ {xs} → ¬ xs < []
+    xs≮[] (base ())
 
     ¬[]<[] : ¬ [] < []
-    ¬[]<[] = xs≮[] []
+    ¬[]<[] = xs≮[]
 
     <-irreflexive : Irreflexive _≈_ _≺_ → Irreflexive _≋_ _<_
     <-irreflexive irr (x≈y ∷ xs≋ys) (this x<y)     = irr x≈y x<y

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

@@ -69,11 +69,11 @@ module _ {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where
     _≋_ = Pointwise _≈_
     _<_ = Lex-< _≈_ _≺_
 
-  xs≮[] : ∀ {n} (xs : Vec A n) → ¬ xs < []
-  xs≮[] _ (base ())
+  xs≮[] : ∀ {n} {xs : Vec A n} → ¬ xs < []
+  xs≮[] (base ())
 
   ¬[]<[] : ¬ [] < []
-  ¬[]<[] = xs≮[] []
+  ¬[]<[] = xs≮[]
 
   module _ (≺-irrefl : Irreflexive _≈_ _≺_) where
 
@@ -134,7 +134,7 @@ module _ {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where
     where
 
     <-wellFounded : ∀ {n} → WellFounded (_<_ {n})
-    <-wellFounded {0}     [] = acc λ ys ys<[] → ⊥-elim (xs≮[] ys ys<[])
+    <-wellFounded {0}     [] = acc λ ys ys<[] → ⊥-elim (xs≮[] ys<[])
     <-wellFounded {suc n} xs = Subrelation.wellFounded <⇒uncons-Lex uncons-Lex-wellFounded xs
       where
         <⇒uncons-Lex : {xs ys : Vec A (suc n)} → xs < ys → (×-Lex _≈_ _≺_ _<_ on uncons) xs ys