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

fix(library/init/data/array/basic): fix and rename eraseIdxSz ==> eraseIdx'

Browse source
This commit is contained in:
Leonardo de Moura 2019-08-02 14:06:35 -07:00
parent 0a86911bd0
commit 84c4637722
2 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/init/data/array/basic.lean
View file

@ -472,8 +472,8 @@ partial def eraseIdxSzAux {α} (a : Array α) : ∀ (i : Nat) (r : Array α), r.
⟨r.pop, (szPopEq r).trans (heq ▸ rfl)⟩
end
def eraseIdxSz {α} (a : Array α) (i : Nat) : { r : Array α // r.size = a.size - 1 } :=
eraseIdxSzAux a i a rfl
def eraseIdx' {α} (a : Array α) (i : Fin a.size) : { r : Array α // r.size = a.size - 1 } :=
eraseIdxSzAux a (i.val + 1) a rfl
end Array

4
library/init/data/persistenthashmap/basic.lean
View file

@ -175,8 +175,8 @@ partial def eraseAux [HasBeq α] : Node α β → USize → α → Node α β ×
| n@(Node.collision keys vals heq) _ k :=
match keys.indexOf k with
| some idx =>
let ⟨keys', keq⟩ := keys.eraseIdxSz idx.val;
let ⟨vals', veq⟩ := vals.eraseIdxSz idx.val;
let ⟨keys', keq⟩ := keys.eraseIdx' idx;
let ⟨vals', veq⟩ := vals.eraseIdx' (Eq.rec idx heq);
have keys.size - 1 = vals.size - 1 from heq ▸ rfl;
(Node.collision keys' vals' (keq.trans (this.trans veq.symm)), true)
| none => (n, false)