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

chore: argument name

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-18 16:19:44 -07:00
parent 3b8c4ada75
commit 7fa43216f5
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Std/Data/PersistentArray.lean
View file

@ -241,8 +241,8 @@ forMAux f t.root *> t.tail.forM f
end
@[inline] def foldl {β} (t : PersistentArray α) (f : β → α → β) (b : β) : β :=
Id.run (t.foldlM f b)
@[inline] def foldl {β} (t : PersistentArray α) (f : β → α → β) (init : β) : β :=
Id.run (t.foldlM f init)
@[inline] def filter (as : PersistentArray α) (p : α → Bool) : PersistentArray α :=
as.foldl (fun asNew a => if p a then asNew.push a else asNew) {}