Changes explicit argument y to implicit in Induction.WellFounded.WfRec

CHANGELOG.md

@@ -551,6 +551,22 @@ Non-backwards compatible changes
  Prime n = ∀ {d} → 2 ≤ d → d < n → d ∤ n
  ```
 
+### Change to the definition of `Induction.WellFounded.WfRec` (issue #2083)
+
+* Previously, the following definition was adopted
+ ```agda
+ WfRec : Rel A r → ∀ {ℓ} → RecStruct A ℓ _
+ WfRec _<_ P x = ∀ y → y < x → P y
+ ```
+ with the consequence that all arguments involving about accesibility and
+ wellfoundedness proofs were polluted by almost-always-inferrable explicit
+ arguments for the `y` position. The definition has now been changed to
+ make that argument *implicit*, as 
+ ```agda
+ WfRec : Rel A r → ∀ {ℓ} → RecStruct A ℓ _
+ WfRec _<_ P x = ∀ {y} → y < x → P y
+ ```
+
 ### Renaming of `Reflection` modules
 
 * Under the `Reflection` module, there were various impending name clashes

README/Data/Nat/Induction.agda

@@ -14,6 +14,14 @@ open import Function.Base using (_∘_)
 open import Induction.WellFounded
 open import Relation.Binary.PropositionalEquality
 
+private
+
+ n<′1+n : ∀ {n} → n <′ suc n
+ n<′1+n = ≤′-refl
+
+ n<′2+n : ∀ {n} → n <′ suc (suc n)
+ n<′2+n = ≤′-step ≤′-refl
+
 -- Doubles its input.
 
 twice : ℕ → ℕ
@@ -46,7 +54,7 @@ mutual
  half₂-step = λ
  { zero _ → zero
  ; (suc zero) _ → zero
- ; (suc (suc n)) rec → suc (rec n (≤′-step ≤′-refl))
+ ; (suc (suc n)) rec → suc (rec n<′2+n)
  }
 
  half₂ : ℕ → ℕ
@@ -92,21 +100,21 @@ half₂-2+ n = begin
 
  half₂-step (2 + n) (<′-recBuilder _ half₂-step (2 + n)) ≡⟨⟩
 
- 1 + <′-recBuilder _ half₂-step (2 + n) n (≤′-step ≤′-refl) ≡⟨⟩
+ 1 + <′-recBuilder _ half₂-step (2 + n) n<′2+n ≡⟨⟩
 
  1 + Some.wfRecBuilder _ half₂-step (2 + n)
- (<′-wellFounded (2 + n)) n (≤′-step ≤′-refl) ≡⟨⟩
+ (<′-wellFounded (2 + n)) n<′2+n ≡⟨⟩
 
  1 + Some.wfRecBuilder _ half₂-step (2 + n)
- (acc (<′-wellFounded′ (2 + n))) n (≤′-step ≤′-refl) ≡⟨⟩
+ (acc (<′-wellFounded′ (2 + n))) n<′2+n ≡⟨⟩
 
  1 + half₂-step n
  (Some.wfRecBuilder _ half₂-step n
- (<′-wellFounded′ (2 + n) n (≤′-step ≤′-refl))) ≡⟨⟩
+ (<′-wellFounded′ (2 + n) n<′2+n)) ≡⟨⟩
 
  1 + half₂-step n
  (Some.wfRecBuilder _ half₂-step n
- (<′-wellFounded′ (1 + n) n ≤′-refl)) ≡⟨⟩
+ (<′-wellFounded′ (1 + n) n<′1+n)) ≡⟨⟩
 
  1 + half₂-step n
  (Some.wfRecBuilder _ half₂-step n (<′-wellFounded n)) ≡⟨⟩
@@ -146,14 +154,14 @@ half₁-+₂ = <′-rec _ λ
  { zero _ → refl
  ; (suc zero) _ → refl
  ; (suc (suc n)) rec →
- cong (suc ∘ suc) (rec n (≤′-step ≤′-refl))
+ cong (suc ∘ suc) (rec n<′2+n)
  }
 
 half₂-+₂ : ∀ n → half₂ (twice n) ≡ n
 half₂-+₂ = <′-rec _ λ
  { zero _ → refl
  ; (suc zero) _ → refl
  ; (suc (suc n)) rec →
- cong (suc ∘ suc) (rec n (≤′-step ≤′-refl))
+ cong (suc ∘ suc) (rec n<′2+n)
  }
 

src/Codata/Musical/Colist/Infinite-merge.agda

@@ -178,7 +178,7 @@ module _ {a p} {A : Set a} {P : A → Set p} where
 
  to : ∀ xss p → Pred (xss , p)
  to = λ xss p →
- WF.All.wfRec (On.wellFounded size <′-wellFounded) _
+ WF.All.wfRec (On.wellFounded size <′-wellFounded)
  Pred step (xss , p)
  where
  size : Input → ℕ
@@ -195,7 +195,7 @@ module _ {a p} {A : Set a} {P : A → Set p} where
  ... | inj₂ q | P.refl | q≤p =
  Prod.map there
  (P.cong (there ∘ _⟨$⟩_ (Inverse.from (Any-⋎P xs)) ∘ inj₂))
- (rec (♭ xss , q) (s≤′s q≤p))
+ (rec {♭ xss , q} (s≤′s q≤p))
 
  to∘from = λ p → from-injective _ _ (proj₂ (to xss (from p)))
 

src/Data/Bool/Properties.agda

@@ -197,8 +197,8 @@ true <? _ = no (λ())
 <-wellFounded : WellFounded _<_
 <-wellFounded _ = acc <-acc
  where
- <-acc : ∀ {x} y → y < x → Acc _<_ y
- <-acc false f<t = acc (λ _ → λ())
+ <-acc : ∀ {x y} → y < x → Acc _<_ y
+ <-acc f<t = acc λ ()
 
 -- Structures
 

src/Data/Digit.agda

@@ -56,7 +56,7 @@ toNatDigits base@(suc (suc _)) n = aux (<-wellFounded-fast n) []
  aux {zero} _ xs = (0 ∷ xs)
  aux {n@(suc _)} (acc wf) xs with does (0 <? n / base)
  ... | false = (n % base) ∷ xs
- ... | true = aux (wf (n / base) q<n) ((n % base) ∷ xs)
+ ... | true = aux (wf q<n) ((n % base) ∷ xs)
  where
  q<n : n / base < n
  q<n = m/n<m n base (s<s z<s)
@@ -107,9 +107,8 @@ toDigits base@(suc (suc k)) n = <′-rec Pred helper n
 
  helper : ∀ n → <′-Rec Pred n → Pred n
  helper n rec with n divMod base
- helper .(toℕ r + 0 * base) rec | result zero r refl = ([ r ] , refl)
- helper .(toℕ r + suc x * base) rec | result (suc x) r refl =
- cons r (rec (suc x) (lem x k (toℕ r)))
+ ... | result zero r eq = ([ r ] , P.sym eq)
+ ... | result (suc x) r refl = cons r (rec (lem x k (toℕ r)))
 
 ------------------------------------------------------------------------
 -- Showing digits

src/Data/Fin/Induction.agda

@@ -65,7 +65,7 @@ open WF public using (Acc; acc)
  induct {suc j} (acc rs) (tri< (s≤s i≤j) _ _) _ = Pᵢ⇒Pᵢ₊₁ j P[1+j]
  where
  toℕj≡toℕinjJ = sym $ toℕ-inject₁ j
- P[1+j] = induct (rs _ (s≤s (subst (ℕ._≤ toℕ j) toℕj≡toℕinjJ ≤-refl)))
+ P[1+j] = induct (rs (s≤s (subst (ℕ._≤ toℕ j) toℕj≡toℕinjJ ≤-refl)))
  (<-cmp i $ inject₁ j) (subst (toℕ i ℕ.≤_) toℕj≡toℕinjJ i≤j)
 
 <-weakInduction : (P : Pred (Fin (suc n)) ℓ) →
@@ -80,8 +80,8 @@ open WF public using (Acc; acc)
 
 private
  acc-map : ∀ {x : Fin n} → Acc ℕ._<_ (n ∸ toℕ x) → Acc _>_ x
- acc-map {n} (acc rs) = acc λ y y>x →
- acc-map (rs (n ∸ toℕ y) (ℕ.∸-monoʳ-< y>x (toℕ≤n y)))
+ acc-map {n} (acc rs) = acc λ {y} y>x →
+ acc-map (rs {n ∸ toℕ y} (ℕ.∸-monoʳ-< y>x (toℕ≤n y)))
 
 >-wellFounded : WellFounded {A = Fin n} _>_
 >-wellFounded {n} x = acc-map (ℕ.<-wellFounded (n ∸ toℕ x))
@@ -96,7 +96,7 @@ private
  induct {i} (acc rec) with n ℕ.≟ toℕ i
  ... | yes n≡i = subst P (toℕ-injective (trans (toℕ-fromℕ n) n≡i)) Pₙ
  ... | no n≢i = subst P (inject₁-lower₁ i n≢i) (Pᵢ₊₁⇒Pᵢ _ Pᵢ₊₁)
- where Pᵢ₊₁ = induct (rec _ (ℕ.≤-reflexive (cong suc (sym (toℕ-lower₁ i n≢i)))))
+ where Pᵢ₊₁ = induct (rec (ℕ.≤-reflexive (cong suc (sym (toℕ-lower₁ i n≢i)))))
 
 ------------------------------------------------------------------------
 -- Well-foundedness of other (strict) partial orders on Fin
@@ -120,7 +120,7 @@ module _ {_≈_ : Rel (Fin n) ℓ} where
  ((xs : Vec (Fin n) m) → Linked (flip _⊏_) (i ∷ xs) → WellFounded _⊏_) →
  Acc _⊏_ i
  go zero i k = k [] [-] i
- go (suc m) i k = acc $ λ j j⊏i → go m j (λ xs i∷xs↑ → k (j ∷ xs) (j⊏i ∷ i∷xs↑))
+ go (suc m) i k = acc λ {j} j⊏i → go m j (λ xs i∷xs↑ → k (j ∷ xs) (j⊏i ∷ i∷xs↑))
 
  pigeon : (xs : Vec (Fin n) n) → Linked (flip _⊏_) (i ∷ xs) → WellFounded _⊏_
  pigeon xs i∷xs↑ =
@@ -161,7 +161,7 @@ module _ {_≈_ : Rel (Fin n) ℓ} where
 ≺-wellFounded = Subrelation.wellFounded ≺⇒<′ ℕ.<′-wellFounded
 
 module _ {ℓ} where
- open WF.All ≺-wellFounded ℓ public
+ open WF.All ≺-wellFounded {ℓ} public
  renaming
  ( wfRecBuilder to ≺-recBuilder
  ; wfRec to ≺-rec

src/Data/Graph/Acyclic.agda

@@ -313,7 +313,7 @@ module _ {ℓ e} {N : Set ℓ} {E : Set e} where
  expand n rec (c & g) =
  node (label c)
  (List.map
- (Prod.map id (λ i → rec (n - suc i) (lemma n i) (g [ i ])))
+ (Prod.map id (λ i → rec {n - suc i} (lemma n i) (g [ i ])))
  (successors c))
 
 -- Performs the toTree expansion once for each node.

src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda

@@ -382,15 +382,18 @@ split v as bs p = helper as bs p (<-wellFounded (steps p))
  helper (a ∷ []) bs (refl eq) _ = [ a ] , bs , eq
  helper (a ∷ b ∷ as) bs (refl eq) _ = a ∷ b ∷ as , bs , eq
  helper [] bs (prep v≈x _) _ = [] , _ , v≈x ∷ ≋-refl
- helper (a ∷ as) bs (prep eq as↭xs) (acc rec) with helper as bs as↭xs (rec _ ≤-refl)
- ... | (ps , qs , eq₂) = a ∷ ps , qs , eq ∷ eq₂
+ helper (a ∷ as) bs (prep eq as↭xs) (acc rec)
+ with ps , qs , eq₂ ← helper as bs as↭xs (rec (n<1+n _))
+ = a ∷ ps , qs , eq ∷ eq₂
  helper [] (b ∷ bs) (swap x≈b y≈v _) _ = [ b ] , _ , x≈b ∷ y≈v ∷ ≋-refl
  helper (a ∷ []) bs (swap x≈v y≈a ↭) _ = [] , a ∷ _ , x≈v ∷ y≈a ∷ ≋-refl
- helper (a ∷ b ∷ as) bs (swap x≈b y≈a as↭xs) (acc rec) with helper as bs as↭xs (rec _ ≤-refl)
- ... | (ps , qs , eq) = b ∷ a ∷ ps , qs , x≈b ∷ y≈a ∷ eq
- helper as bs (trans ↭₁ ↭₂) (acc rec) with helper as bs ↭₂ (rec _ (m<n+m (steps ↭₂) (0<steps ↭₁)))
- ... | (ps , qs , eq) = helper ps qs (↭-respʳ-≋ eq ↭₁)
- (rec _ (subst (_< _) (sym (steps-respʳ eq ↭₁)) (m<m+n (steps ↭₁) (0<steps ↭₂))))
+ helper (a ∷ b ∷ as) bs (swap x≈b y≈a as↭xs) (acc rec)
+ with ps , qs , eq ← helper as bs as↭xs (rec (n<1+n _))
+ = b ∷ a ∷ ps , qs , x≈b ∷ y≈a ∷ eq
+ helper as bs (trans ↭₁ ↭₂) (acc rec)
+ with ps , qs , eq ← helper as bs ↭₂ (rec (m<n+m (steps ↭₂) (0<steps ↭₁)))
+ = helper ps qs (↭-respʳ-≋ eq ↭₁)
+ (rec (subst (_< _) (sym (steps-respʳ eq ↭₁)) (m<m+n (steps ↭₁) (0<steps ↭₂))))
 
 ------------------------------------------------------------------------
 -- filter

src/Data/List/Sort/MergeSort.agda

@@ -44,20 +44,20 @@ open PermutationReasoning
 -- Definition
 
 mergePairs : List (List A) → List (List A)
-mergePairs (xs ∷ ys ∷ xss) = merge _≤?_ xs ys ∷ mergePairs xss
+mergePairs (xs ∷ ys ∷ yss) = merge _≤?_ xs ys ∷ mergePairs yss
 mergePairs xss = xss
 
 private
- length-mergePairs : ∀ xs ys xss → length (mergePairs (xs ∷ ys ∷ xss)) < length (xs ∷ ys ∷ xss)
+ length-mergePairs : ∀ xs ys yss → length (mergePairs (xs ∷ ys ∷ yss)) < length (xs ∷ ys ∷ yss)
  length-mergePairs _ _ [] = s<s z<s
- length-mergePairs _ _ (xss ∷ []) = s<s (s<s z<s)
- length-mergePairs _ _ (xs ∷ ys ∷ xss) = s<s (m<n⇒m<1+n (length-mergePairs xs ys xss))
+ length-mergePairs _ _ (xs ∷ [])  = s<s (s<s z<s)
+ length-mergePairs _ _ (xs ∷ ys ∷ yss) = s<s (m<n⇒m<1+n (length-mergePairs xs ys yss))
 
 mergeAll : (xss : List (List A)) → Acc _<_ (length xss) → List A
 mergeAll [] _ = []
 mergeAll (xs ∷ []) _ = xs
-mergeAll (xs ∷ ys ∷ xss) (acc rec) = mergeAll
- (mergePairs (xs ∷ ys ∷ xss)) (rec _ (length-mergePairs xs ys xss))
+mergeAll xss@(xs ∷ ys ∷ yss) (acc rec) = mergeAll
+ (mergePairs xss) (rec (length-mergePairs xs ys yss))
 
 sort : List A → List A
 sort xs = mergeAll (map [_] xs) (<-wellFounded-fast _)

src/Data/Nat/DivMod.agda

@@ -294,7 +294,7 @@ m*n/m*o≡n/o m@(suc _) n o = helper (<-wellFounded n)
  ... | no n≮o = begin-equality
  (m * n) / (m * o) ≡⟨ m/n≡1+[m∸n]/n (*-monoʳ-≤ m (≮⇒≥ n≮o)) ⟩
  1 + (m * n ∸ m * o) / (m * o) ≡˘⟨ cong (λ v → 1 + v / (m * o)) (*-distribˡ-∸ m n o) ⟩
- 1 + (m * (n ∸ o)) / (m * o) ≡⟨ cong suc (helper (rec (n ∸ o) n∸o<n)) ⟩
+ 1 + (m * (n ∸ o)) / (m * o) ≡⟨ cong suc (helper (rec n∸o<n)) ⟩
  1 + (n ∸ o) / o ≡˘⟨ cong₂ _+_ (n/n≡1 o) refl ⟩
  o / o + (n ∸ o) / o ≡˘⟨ +-distrib-/-∣ˡ (n ∸ o) (divides 1 ((sym (*-identityˡ o)))) ⟩
  (o + (n ∸ o)) / o ≡⟨ cong (_/ o) (m+[n∸m]≡n (≮⇒≥ n≮o)) ⟩

src/Data/Nat/GCD.agda

@@ -43,7 +43,7 @@ open import Algebra.Definitions {A = ℕ} _≡_ as Algebra
 
 gcd′ : ∀ m n → Acc _<_ m → n < m → ℕ
 gcd′ m zero _ _ = m
-gcd′ m n@(suc _) (acc rec) n<m = gcd′ n (m % n) (rec _ n<m) (m%n<n m n)
+gcd′ m n@(suc _) (acc rec) n<m = gcd′ n (m % n) (rec n<m) (m%n<n m n)
 
 gcd : ℕ → ℕ → ℕ
 gcd m n with <-cmp m n
@@ -55,15 +55,15 @@ gcd m n with <-cmp m n
 -- Core properties of gcd′
 
 gcd′[m,n]∣m,n : ∀ {m n} rec n<m → gcd′ m n rec n<m ∣ m × gcd′ m n rec n<m ∣ n
-gcd′[m,n]∣m,n {m} {zero} rec n<m = ∣-refl , m ∣0
-gcd′[m,n]∣m,n {m} {suc n} (acc rec) n<m
- with gcd∣n , gcd∣m%n ← gcd′[m,n]∣m,n (rec _ n<m) (m%n<n m (suc n))
+gcd′[m,n]∣m,n {m} {zero}  rec n<m = ∣-refl , m ∣0
+gcd′[m,n]∣m,n {m} {n@(suc _)} (acc rec) n<m
+ with gcd∣n , gcd∣m%n ← gcd′[m,n]∣m,n (rec n<m) (m%n<n m n)
  = ∣n∣m%n⇒∣m gcd∣n gcd∣m%n , gcd∣n
 
 gcd′-greatest : ∀ {m n c} rec n<m → c ∣ m → c ∣ n → c ∣ gcd′ m n rec n<m
-gcd′-greatest {m} {zero} rec n<m c∣m c∣n = c∣m
-gcd′-greatest {m} {suc n} (acc rec) n<m c∣m c∣n =
- gcd′-greatest (rec _ n<m) (m%n<n m (suc n)) c∣n (%-presˡ-∣ c∣m c∣n)
+gcd′-greatest {m} {zero}  rec n<m c∣m c∣n = c∣m
+gcd′-greatest {m} {n@(suc _)} (acc rec) n<m c∣m c∣n =
+ gcd′-greatest (rec n<m) (m%n<n m n) c∣n (%-presˡ-∣ c∣m c∣n)
 
 ------------------------------------------------------------------------
 -- Core properties of gcd
@@ -387,13 +387,13 @@ module Bézout where
  P (m , n) = Lemma m n
 
  gcd″ : ∀ p → (<′-Rec ⊗ <′-Rec) P p → P p
- gcd″ (zero , n) rec = Lemma.base n
- gcd″ (suc m , zero) rec = Lemma.sym (Lemma.base (suc m))
- gcd″ (suc m , suc n) rec with compare m n
- ... | equal m = Lemma.refl (suc m)
- ... | less m k = Lemma.stepˡ $ proj₁ rec (suc k) (lem₁ k m)
+ gcd″ (zero  , n) rec = Lemma.base n
+ gcd″ (m@(suc _) , zero) rec = Lemma.sym (Lemma.base m)
+ gcd″ (m′@(suc m) , n′@(suc n)) rec with compare m n
+ ... | equal m = Lemma.refl m′
+ ... | less m k = Lemma.stepˡ $ proj₁ rec (lem₁ k m)
  -- "gcd (suc m) (suc k)"
- ... | greater n k = Lemma.stepʳ $ proj₂ rec (suc k) (lem₁ k n) (suc n)
+ ... | greater n k = Lemma.stepʳ $ proj₂ rec (lem₁ k n) n′
  -- "gcd (suc k) (suc n)"
 
  -- Bézout's identity can be recovered from the GCD.

src/Data/Nat/Induction.agda

@@ -67,11 +67,11 @@ cRec = build cRecBuilder
 
 <′-wellFounded n = acc (<′-wellFounded′ n)
 
-<′-wellFounded′ (suc n) n <′-base = <′-wellFounded n
-<′-wellFounded′ (suc n) m (<′-step m<n) = <′-wellFounded′ n m m<n
+<′-wellFounded′ (suc n) <′-base = <′-wellFounded n
+<′-wellFounded′ (suc n) (<′-step m<n) = <′-wellFounded′ n m<n
 
 module _ {ℓ : Level} where
- open WF.All <′-wellFounded ℓ public
+ open WF.All <′-wellFounded {ℓ} public
  renaming ( wfRecBuilder to <′-recBuilder
  ; wfRec to <′-rec
  )
@@ -100,10 +100,10 @@ module _ {ℓ : Level} where
  <-wellFounded-skip : ∀ (k : ℕ) → WellFounded _<_
  <-wellFounded-skip zero n = <-wellFounded n
  <-wellFounded-skip (suc k) zero = <-wellFounded 0
- <-wellFounded-skip (suc k) (suc n) = acc (λ m _ → <-wellFounded-skip k m)
+ <-wellFounded-skip (suc k) (suc n) = acc (λ {m} _ → <-wellFounded-skip k m)
 
 module _ {ℓ : Level} where
- open WF.All <-wellFounded ℓ public
+ open WF.All <-wellFounded {ℓ} public
  renaming ( wfRecBuilder to <-recBuilder
  ; wfRec to <-rec
  )

src/Data/Nat/Logarithm/Core.agda

@@ -23,15 +23,15 @@ open import Data.Unit
 ⌊log2⌋ : ∀ n → Acc _<_ n → ℕ
 ⌊log2⌋ 0 _ = 0
 ⌊log2⌋ 1 _ = 0
-⌊log2⌋ (suc n′@(suc n)) (acc rs) = 1 + ⌊log2⌋ (suc ⌊ n /2⌋) (rs _ (⌊n/2⌋<n n′))
+⌊log2⌋ (suc n′@(suc n)) (acc rs) = 1 + ⌊log2⌋ (suc ⌊ n /2⌋) (rs (⌊n/2⌋<n n′))
 
 
 -- Ceil version
 
 ⌈log2⌉ : ∀ n → Acc _<_ n → ℕ
 ⌈log2⌉ 0 _ = 0
 ⌈log2⌉ 1 _ = 0
-⌈log2⌉ (suc (suc n)) (acc rs) = 1 + ⌈log2⌉ (suc ⌈ n /2⌉) (rs _ (⌈n/2⌉<n n))
+⌈log2⌉ (suc (suc n)) (acc rs) = 1 + ⌈log2⌉ (suc ⌈ n /2⌉) (rs (⌈n/2⌉<n n))
 
 ------------------------------------------------------------------------
 -- Properties of ⌊log2⌋

src/Data/Nat/Properties.agda

@@ -486,7 +486,7 @@ m<1+n⇒m≤n (s≤s m≤n) = m≤n
 ∀[m<n⇒m≢o]⇒n≤o (suc n) (suc o) m<n⇒m≢o = s≤s (∀[m<n⇒m≢o]⇒n≤o n o rec)
  where
  rec : ∀ {m} → m < n → m ≢ o
- rec x<m refl = m<n⇒m≢o (s≤s x<m) refl
+ rec o<n refl = m<n⇒m≢o (s<s o<n) refl
 
 ------------------------------------------------------------------------
 -- A module for reasoning about the _≤_ and _<_ relations

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

@@ -202,13 +202,13 @@ module _ {_≈₁_ : Rel A ℓ₁} {_<₁_ : Rel A ℓ₂} {_<₂_ : Rel B ℓ
  ×-acc : ∀ {x y} →
  Acc _<₁_ x → Acc _<₂_ y →
  WfRec _<ₗₑₓ_ (Acc _<ₗₑₓ_) (x , y)
- ×-acc (acc rec₁) acc₂ (u , v) (inj₁ u<x)
- = acc (×-acc (rec₁ u u<x) (wf₂ v))
- ×-acc acc₁ (acc rec₂) (u , v) (inj₂ (u≈x , v<y))
+ ×-acc (acc rec₁) acc₂ {u , v} (inj₁ u<x)
+ = acc (×-acc (rec₁ {u} u<x) (wf₂ v))
+ ×-acc acc₁ (acc rec₂) (inj₂ (u≈x , v<y))
  = Acc-resp-flip-≈
  (×-respectsʳ {_<₁_ = _<₁_} {_<₂_ = _<₂_} trans resp (≡.respʳ _<₂_))
  (u≈x , ≡.refl)
- (acc (×-acc acc₁ (rec₂ v v<y)))
+ (acc (×-acc acc₁ (rec₂ v<y)))
 
 
 module _ {_<₁_ : Rel A ℓ₁} {_<₂_ : Rel B ℓ₂} where

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

@@ -134,7 +134,8 @@ module _ {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where
  where
 
  <-wellFounded : ∀ {n} → WellFounded (_<_ {n})
- <-wellFounded {0} [] = acc λ ys ys<[] → ⊥-elim (xs≮[] ys<[])
+ <-wellFounded {0} [] = acc λ 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