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

chore: consistency

Browse source 
Make sure `Array.all` and `Array.any` parameter order is similar to
`List.all` and `List.any`.
This commit is contained in:
Leonardo de Moura 2021-02-04 20:39:28 -08:00
parent 8a1433794b
commit d0ffecd419
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/Init/Data/Array/Basic.lean
View file

@ -423,11 +423,11 @@ def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat :=
a.findIdx? fun a => a == v
@[inline]
def any (p : α → Bool) (as : Array α) (start := 0) (stop := as.size) : Bool :=
def any (as : Array α) (p : α → Bool) (start := 0) (stop := as.size) : Bool :=
Id.run <| as.anyM p start stop
@[inline]
def all (p : α → Bool) (as : Array α) (start := 0) (stop := as.size) : Bool :=
def all (as : Array α) (p : α → Bool) (start := 0) (stop := as.size) : Bool :=
Id.run <| as.allM p start stop
def contains [BEq α] (as : Array α) (a : α) : Bool :=