From 356db4e1df9ace14ed70fd8831663f12a2a0de8d Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Mon, 19 Sep 2022 15:46:49 -0400 Subject: [PATCH] fix: simplify termination_by clause --- src/Init/Data/Array/Basic.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index 835a421fd8..6a3d1da0a6 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -717,14 +717,13 @@ def erase [BEq α] (as : Array α) (a : α) : Array α := let j := as.size let as := as.push a loop as ⟨j, size_push .. ▸ j.lt_succ_self⟩ -termination_by _ _ _ j => j.1 +termination_by loop j => j.1 /-- Insert element `a` at position `i`. Panics if `i` is not `i ≤ as.size`. -/ def insertAt! (as : Array α) (i : Nat) (a : α) : Array α := if h : i ≤ as.size then insertAt as ⟨i, Nat.lt_succ_of_le h⟩ a else panic! "invalid index" -termination_by _ _ _ j => j.1 def toListLitAux (a : Array α) (n : Nat) (hsz : a.size = n) : ∀ (i : Nat), i ≤ a.size → List α → List α | 0, _, acc => acc