<div dir="ltr"><div>Hi all:</div><div><br></div><div>I've noticed that termination checking has trouble "seeing" through `with` and I'm wondering if there might be some improvements coming down the pike that might help. <br></div><div><br></div><div>As a simple example, compare these two definitions of `merge` from merge sort; the first one is okay and the second one isn't.</div><div><br></div><div>merge : 𝕃 ℕ -> 𝕃 ℕ -> 𝕃 ℕ<br>merge [] l = l<br>merge (x :: l) [] = x :: l<br>merge (x₁ :: l1) (x₂ :: l2) = <br>  if (x₁ < x₂)<br>  then x₁ :: merge l1 (x₂ :: l2)<br>  else x₂ :: merge (x₁ :: l1) l2<br><br><br>merge : 𝕃 ℕ -> 𝕃 ℕ -> 𝕃 ℕ<br>merge [] m = m <br>merge (x :: l) [] = x :: l<br>merge (x :: l) (y :: m) with x < y<br>... | tt = merge l (y :: m)<br>... | ff = merge (x :: l) m</div><div><br></div><div>This also comes up in proofs where the inductive hypothesis has to be bound to a variable before doing a case split (with a `with`).<br></div><div><br></div><div>Robby</div><div><br></div><div>;; --------<br></div><div><br></div><div>The code above is using the IAL; here's a complete agda file without any dependencies in case that's helpful.</div><div><br></div><div>module _ where<br><br>data 𝔹 : Set where<br> tt : 𝔹<br> ff : 𝔹<br><br>infix  4 if_then_else_<br><br>if_then_else_ : ∀ {ℓ} {A : Set ℓ} → 𝔹 → A → A → A<br>if tt then y else z = y<br>if ff then y else z = z<br><br>data 𝕃 {ℓ} (A : Set ℓ) : Set ℓ where<br>  [] : 𝕃 A<br>  _::_ : (x : A) (xs : 𝕃 A) → 𝕃 A<br><br>data ℕ : Set where<br>  zero : ℕ<br>  suc : ℕ → ℕ<br><br>_<_ : ℕ → ℕ → 𝔹<br>zero < zero = ff<br>zero < (suc y) = tt<br>(suc x) < (suc y) = x < y<br>(suc x) < zero = ff<br><br>merge : 𝕃 ℕ -> 𝕃 ℕ -> 𝕃 ℕ<br>merge [] l = l<br>merge (x :: l) [] = x :: l<br>merge (x₁ :: l1) (x₂ :: l2) = <br>  if (x₁ < x₂)<br>  then x₁ :: merge l1 (x₂ :: l2)<br>  else x₂ :: merge (x₁ :: l1) l2<br><br>merge' : 𝕃 ℕ -> 𝕃 ℕ -> 𝕃 ℕ<br>merge' [] m = m <br>merge' (x :: l) [] = x :: l<br>merge' (x :: l) (y :: m) with x < y<br>... | tt = merge' l (y :: m)<br>... | ff = merge' (x :: l) m<br><br><br></div><div><br></div><div><br></div><div><br></div><div><br></div></div>