max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove redundant proof

Browse source
This commit is contained in:
Sebastian Ullrich 2022-03-12 11:12:56 +01:00
parent a4f47adf9e
commit 82c682d385
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Init/Data/Array/Basic.lean
View file

@ -659,7 +659,6 @@ def eraseIdxAux (i : Nat) (a : Array α) : Array α :=
let idx : Fin a.size := ⟨i, h⟩;
let idx1 : Fin a.size := ⟨i - 1, by exact Nat.lt_of_le_of_lt (Nat.pred_le i) h⟩;
let a' := a.swap idx idx1
have : a'.size - (i+1) < a.size - i := by rw [size_swap]; apply Nat.sub_succ_lt_self; assumption
eraseIdxAux (i+1) a'
else
a.pop