From 4b4ff9bf69d0225acf191025fbc8c42d968ae86b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 6 May 2019 18:21:29 -0700
Subject: [PATCH] feat(library/init/data/array/basic): add `Array.mfor`

---
 library/init/data/array/basic.lean | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

diff --git a/library/init/data/array/basic.lean b/library/init/data/array/basic.lean
index 693978f3ec..4d62682e76 100644
--- a/library/init/data/array/basic.lean
+++ b/library/init/data/array/basic.lean
@@ -305,6 +305,25 @@ Id.run $ hmmapAux f 0 a
 @[inline] def map (f : α → β) (as : Array α) : Array β :=
 as.foldl (λ bs a, bs.push (f a)) (mkEmpty as.size)
 
+section
+variables {m : Type u → Type u} [Monad m]
+local attribute [instance] monadInhabited
+
+@[specialize]
+partial def mforAux {α : Type w} {β : Type u} (f : α → m β) (a : Array α) : Nat → m PUnit
+| i :=
+  if h : i < a.size then
+     let idx : Fin a.size := ⟨i, h⟩ in
+     let v   : α          := a.fget idx in
+     f v *> mforAux (i+1)
+  else
+     pure ⟨⟩
+
+def mfor {α : Type w} {β : Type u} (f : α → m β) (a : Array α) : m PUnit :=
+a.mforAux f 0
+
+end
+
 -- TODO(Leo): justify termination using wf-rec
 partial def extractAux (a : Array α) : Nat → Π (e : Nat), e ≤ a.size → Array α → Array α
 | i e hle r :=