From c1fecc89391f0885d75e24244cb2e0094817bb5f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 6 May 2019 13:47:36 -0700
Subject: [PATCH] feat(library/init/data/array/basic): add `anyM` and `allM`

---
 library/init/data/array/basic.lean | 24 ++++++++++++++++++------
 1 file changed, 18 insertions(+), 6 deletions(-)

diff --git a/library/init/data/array/basic.lean b/library/init/data/array/basic.lean
index f1f1a62538..693978f3ec 100644
--- a/library/init/data/array/basic.lean
+++ b/library/init/data/array/basic.lean
@@ -211,17 +211,29 @@ iterate₂ a₁ a₂ b (λ _ a₁ a₂ b, f b a₁ a₂)
 @[inline] def find (a : Array α) (f : α → Option β) : Option β :=
 Id.run $ mfindAux a f 0
 
-@[specialize] partial def anyAux (a : Array α) (p : α → Bool) : Nat → Bool
+section
+variables {m : Type → Type v} [Monad m]
+local attribute [instance] monadInhabited
+
+@[specialize] partial def anyMAux (a : Array α) (p : α → m Bool) : Nat → m Bool
 | i :=
   if h : i < a.size then
      let idx : Fin a.size := ⟨i, h⟩ in
-     match p (a.fget idx) with
-     | true  := true
-     | false := anyAux (i+1)
-  else false
+     do b ← p (a.fget idx),
+     match b with
+     | true  := pure true
+     | false := anyMAux (i+1)
+  else pure false
+
+@[inline] def anyM (a : Array α) (p : α → m Bool) : m Bool :=
+anyMAux a p 0
+
+@[inline] def allM (a : Array α) (p : α → m Bool) : m Bool :=
+not <$> anyM a (λ v, not <$> p v)
+end
 
 @[inline] def any (a : Array α) (p : α → Bool) : Bool :=
-anyAux a p 0
+Id.run $ anyM a p
 
 @[inline] def all (a : Array α) (p : α → Bool) : Bool :=
 !any a (λ v, !p v)