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

feat(library/init/list): add list.any and list.all

Browse source
This commit is contained in:
Leonardo de Moura 2016-10-12 13:30:39 -07:00
parent deb2bb92b2
commit e6acd52fc2
1 changed files with 14 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
library/init/list.lean
View file

@ -111,4 +111,18 @@ def dropn : ℕ → list A → list A
| (succ n) [] := []
| (succ n) (x::r) := dropn n r
definition foldl (f : A → B → A) : A → list B → A
| a [] := a
| a (b :: l) := foldl (f a b) l
definition foldr (f : A → B → B) : B → list A → B
| b [] := b
| b (a :: l) := f a (foldr b l)
definition any (l : list A) (p : A → bool) : bool :=
foldr (λ a r, p a || r) ff l
definition all (l : list A) (p : A → bool) : bool :=
foldr (λ a r, p a && r) tt l
end list