From ab41dd0d83b6df2613d8d3c097704655fc262129 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 11 Feb 2022 09:28:46 -0800
Subject: [PATCH] test: add test for issue #1013

---
 tests/lean/run/overAndPartialAppsAtWF.lean | 23 ++++++++++++++++++++++
 1 file changed, 23 insertions(+)
 create mode 100644 tests/lean/run/overAndPartialAppsAtWF.lean

diff --git a/tests/lean/run/overAndPartialAppsAtWF.lean b/tests/lean/run/overAndPartialAppsAtWF.lean
new file mode 100644
index 0000000000..615728e933
--- /dev/null
+++ b/tests/lean/run/overAndPartialAppsAtWF.lean
@@ -0,0 +1,23 @@
+theorem eq_of_isEqvAux [DecidableEq α] (a b : Array α) (hsz : a.size = b.size) (i : Nat) (hi : i ≤ a.size) (heqv : Array.isEqvAux a b hsz (fun x y => x = y) i) : ∀ (j : Nat) (hl : i ≤ j) (hj : j < a.size), a.get ⟨j, hj⟩ = b.get ⟨j, hsz ▸ hj⟩ := by
+  intro j low high
+  by_cases h : i < a.size
+  . unfold Array.isEqvAux at heqv
+    simp [h] at heqv
+    have hind := eq_of_isEqvAux a b hsz (i+1) (Nat.succ_le_of_lt h) heqv.2
+    by_cases heq : i = j
+    . subst heq; exact heqv.1
+    . exact hind j (Nat.succ_le_of_lt (Nat.lt_of_le_and_ne low heq)) high
+  . have heq : i = a.size := Nat.le_antisymm hi (Nat.ge_of_not_lt h)
+    subst heq
+    exact absurd (Nat.lt_of_lt_of_le high low) (Nat.lt_irrefl j)
+termination_by _ => a.size - i
+
+@[simp] def f (x y : Nat) : Nat → Nat :=
+  if h : x > 0 then
+    fun z => f (x - 1) (y + 1) z + 1
+  else
+    (. + y)
+termination_by
+  f x y => x
+
+#check f._eq_1