Looks like something got inlined

leanprover · Aug 15, 2024 · 4d81004 · 4d81004
1 parent bcf5fd8
commit 4d81004
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/tests/lean/run/986.lean b/tests/lean/run/986.lean
@@ -11,8 +11,7 @@ info: Array.insertionSort.swapLoop.eq_1.{u_1} {α : Type u_1} (lt : α → α
 info: Array.insertionSort.swapLoop.eq_2.{u_1} {α : Type u_1} (lt : α → α → Bool) (a : Array α) (j' : Nat)
   (h : j'.succ < a.size) :
   Array.insertionSort.swapLoop lt a j'.succ h =
-    let_fun h' := ⋯;
-    if lt a[j'.succ] a[j'] = true then Array.insertionSort.swapLoop lt (a.swap ⟨j'.succ, h⟩ ⟨j', h'⟩) j' ⋯ else a
+    if lt a[j'.succ] a[j'] = true then Array.insertionSort.swapLoop lt (a.swap ⟨j'.succ, h⟩ ⟨j', ⋯⟩) j' ⋯ else a
 -/
 #guard_msgs in
 #check Array.insertionSort.swapLoop.eq_2