From 34765c97d7b34b491816bb89c952536a12801d8b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 27 Oct 2019 18:19:34 -0700
Subject: [PATCH] chore: rename `mmap`, `mfoldl`, `mfor` ...

We now use `mapM`, `foldlM`, ... like Haskell.
Motivation: fixes the inconsistent naming convetion. We are already
using the `M` suffix for functions such as `anyM`. We used `anyM`
because `many` is a valid English word.

cc @kha @dselsam
---
 library/Init/Control/Combinators.lean         |  78 ++++++-------
 library/Init/Data/Array/Basic.lean            | 105 +++++++++---------
 library/Init/Data/AssocList.lean              |   6 +-
 library/Init/Data/HashMap/Basic.lean          |  14 +--
 library/Init/Data/HashSet.lean                |   6 +-
 library/Init/Data/PersistentArray/Basic.lean  |  82 +++++++-------
 .../Init/Data/PersistentHashMap/Basic.lean    |  14 +--
 library/Init/Data/PersistentHashSet.lean      |   6 +-
 library/Init/Lean/AbstractMetavarContext.lean |   4 +-
 library/Init/Lean/Attributes.lean             |   8 +-
 library/Init/Lean/Compiler/IR/Basic.lean      |   2 +-
 library/Init/Lean/Compiler/IR/Borrow.lean     |  20 ++--
 library/Init/Lean/Compiler/IR/Boxing.lean     |   8 +-
 library/Init/Lean/Compiler/IR/Checker.lean    |   8 +-
 library/Init/Lean/Compiler/IR/CompilerM.lean  |   2 +-
 library/Init/Lean/Compiler/IR/Default.lean    |   2 +-
 .../Lean/Compiler/IR/ElimDeadBranches.lean    |  10 +-
 library/Init/Lean/Compiler/IR/EmitC.lean      |  44 ++++----
 library/Init/Lean/Compiler/IR/EmitUtil.lean   |   2 +-
 .../Lean/Compiler/IR/ExpandResetReuse.lean    |   4 +-
 library/Init/Lean/Compiler/IR/NormIds.lean    |   4 +-
 library/Init/Lean/Compiler/IR/ResetReuse.lean |   4 +-
 library/Init/Lean/Elaborator/Basic.lean       |   4 +-
 library/Init/Lean/Elaborator/Command.lean     |   2 +-
 library/Init/Lean/Elaborator/PreTerm.lean     |  10 +-
 library/Init/Lean/Elaborator/Term.lean        |   2 +-
 library/Init/Lean/Environment.lean            |  12 +-
 library/Init/Lean/LocalContext.lean           |  28 ++---
 library/Init/Lean/Parser/Module.lean          |   4 +-
 library/Init/Lean/Path.lean                   |   4 +-
 library/Init/Lean/Syntax.lean                 |   8 +-
 library/Init/Lean/Trace.lean                  |   2 +-
 library/Init/Lean/TypeClass/Context.lean      |   4 +-
 library/Init/Lean/TypeClass/Synth.lean        |   2 +-
 34 files changed, 257 insertions(+), 258 deletions(-)

diff --git a/library/Init/Control/Combinators.lean b/library/Init/Control/Combinators.lean
index 349b482c46..c861c3247e 100644
--- a/library/Init/Control/Combinators.lean
+++ b/library/Init/Control/Combinators.lean
@@ -12,7 +12,7 @@ import Init.Data.List.Basic
 
 universes u v w u₁ u₂ u₃
 
-def mjoin {m : Type u → Type u} [Monad m] {α : Type u} (a : m (m α)) : m α :=
+def joinM {m : Type u → Type u} [Monad m] {α : Type u} (a : m (m α)) : m α :=
 bind a id
 
 @[macroInline]
@@ -24,42 +24,42 @@ def unless {m : Type → Type u} [Applicative m] (c : Prop) [h : Decidable c] (e
 if c then pure () else e
 
 @[macroInline]
-def mcond {m : Type → Type u} [Monad m] {α : Type} (mbool : m Bool) (tm fm : m α) : m α :=
+def condM {m : Type → Type u} [Monad m] {α : Type} (mbool : m Bool) (tm fm : m α) : m α :=
 do b ← mbool; cond b tm fm
 
 @[macroInline]
-def mwhen {m : Type → Type u} [Monad m] (c : m Bool) (t : m Unit) : m Unit :=
-mcond c t (pure ())
+def whenM {m : Type → Type u} [Monad m] (c : m Bool) (t : m Unit) : m Unit :=
+condM c t (pure ())
 
 namespace Nat
 
-@[specialize] def mforAux {m} [Applicative m] (f : Nat → m Unit) (n : Nat) : Nat → m Unit
+@[specialize] def forMAux {m} [Applicative m] (f : Nat → m Unit) (n : Nat) : Nat → m Unit
 | 0   => pure ()
-| i+1 => f (n-i-1) *> mforAux i
+| i+1 => f (n-i-1) *> forMAux i
 
-@[inline] def mfor {m} [Applicative m] (n : Nat) (f : Nat → m Unit) : m Unit :=
-mforAux f n n
+@[inline] def forM {m} [Applicative m] (n : Nat) (f : Nat → m Unit) : m Unit :=
+forMAux f n n
 
-@[specialize] def mforRevAux {m} [Applicative m] (f : Nat → m Unit) : Nat → m Unit
+@[specialize] def forRevMAux {m} [Applicative m] (f : Nat → m Unit) : Nat → m Unit
 | 0   => pure ()
-| i+1 => f i *> mforRevAux i
+| i+1 => f i *> forRevMAux i
 
-@[inline] def mforRev {m} [Applicative m] (n : Nat) (f : Nat → m Unit) : m Unit :=
-mforRevAux f n
+@[inline] def forRevM {m} [Applicative m] (n : Nat) (f : Nat → m Unit) : m Unit :=
+forRevMAux f n
 
-@[specialize] def mfoldAux {α : Type u} {m : Type u → Type v} [Monad m] (f : Nat → α → m α) (n : Nat) : Nat → α → m α
+@[specialize] def foldMAux {α : Type u} {m : Type u → Type v} [Monad m] (f : Nat → α → m α) (n : Nat) : Nat → α → m α
 | 0,   a => pure a
-| i+1, a => f (n-i-1) a >>= mfoldAux i
+| i+1, a => f (n-i-1) a >>= foldMAux i
 
-@[inline] def mfold {α : Type u} {m : Type u → Type v} [Monad m] (f : Nat → α → m α) (a : α) (n : Nat) : m α :=
-mfoldAux f n n a
+@[inline] def foldM {α : Type u} {m : Type u → Type v} [Monad m] (f : Nat → α → m α) (a : α) (n : Nat) : m α :=
+foldMAux f n n a
 
-@[specialize] def mfoldRevAux {α : Type u} {m : Type u → Type v} [Monad m] (f : Nat → α → m α) : Nat → α → m α
+@[specialize] def foldRevMAux {α : Type u} {m : Type u → Type v} [Monad m] (f : Nat → α → m α) : Nat → α → m α
 | 0,   a => pure a
-| i+1, a => f i a >>= mfoldRevAux i
+| i+1, a => f i a >>= foldRevMAux i
 
 @[inline] def mfoldRev {α : Type u} {m : Type u → Type v} [Monad m] (f : Nat → α → m α) (a : α) (n : Nat) : m α :=
-mfoldRevAux f n a
+foldRevMAux f n a
 
 -- TODO: enable after we have support for marking arguments that should be considered for specialization.
 /-
@@ -73,61 +73,61 @@ end Nat
 namespace List
 
 @[specialize]
-def mmap {m : Type u → Type v} [Applicative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m (List β)
+def mapM {m : Type u → Type v} [Applicative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m (List β)
 | []    => pure []
-| a::as => List.cons <$> (f a) <*> mmap as
+| a::as => List.cons <$> (f a) <*> mapM as
 
 @[specialize]
-def mmap₂ {m : Type u → Type v} [Applicative m] {α : Type u₁} {β : Type u₂} {γ : Type u} (f : α → β → m γ) : List α → List β → m (List γ)
-| a::as, b::bs => List.cons <$> (f a b) <*> mmap₂ as bs
+def mapM₂ {m : Type u → Type v} [Applicative m] {α : Type u₁} {β : Type u₂} {γ : Type u} (f : α → β → m γ) : List α → List β → m (List γ)
+| a::as, b::bs => List.cons <$> (f a b) <*> mapM₂ as bs
 | _,     _     => pure []
 
 @[specialize]
-def mfor {m : Type u → Type v} [Applicative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m PUnit
+def forM {m : Type u → Type v} [Applicative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m PUnit
 | []     => pure ⟨⟩
-| h :: t => f h *> mfor t
+| h :: t => f h *> forM t
 
 @[specialize]
-def mfor₂ {m : Type u → Type v} [Applicative m] {α : Type u₁} {β : Type u₂} {γ : Type u} (f : α → β → m γ) : List α → List β → m PUnit
-| a::as, b::bs => f a b *> mfor₂ as bs
+def forM₂ {m : Type u → Type v} [Applicative m] {α : Type u₁} {β : Type u₂} {γ : Type u} (f : α → β → m γ) : List α → List β → m PUnit
+| a::as, b::bs => f a b *> forM₂ as bs
 | _,     _     => pure ⟨⟩
 
 @[specialize]
-def mfilter {m : Type → Type v} [Monad m] {α : Type} (f : α → m Bool) : List α → m (List α)
+def filterM {m : Type → Type v} [Monad m] {α : Type} (f : α → m Bool) : List α → m (List α)
 | []     => pure []
-| h :: t => do b ← f h; t' ← mfilter t; cond b (pure (h :: t')) (pure t')
+| h :: t => do b ← f h; t' ← filterM t; cond b (pure (h :: t')) (pure t')
 
 @[specialize]
-def mfoldl {m : Type u → Type v} [Monad m] {s : Type u} {α : Type w} : (s → α → m s) → s → List α → m s
+def foldlM {m : Type u → Type v} [Monad m] {s : Type u} {α : Type w} : (s → α → m s) → s → List α → m s
 | f, s, [] => pure s
 | f, s, h :: r   => do
   s' ← f s h;
-  mfoldl f s' r
+  foldlM f s' r
 
 @[specialize]
-def mfoldr {m : Type u → Type v} [Monad m] {s : Type u} {α : Type w} : (α → s → m s) → s → List α → m s
+def foldrM {m : Type u → Type v} [Monad m] {s : Type u} {α : Type w} : (α → s → m s) → s → List α → m s
 | f, s, [] => pure s
 | f, s, h :: r   => do
-  s' ← mfoldr f s r;
+  s' ← foldrM f s r;
   f h s'
 
 @[specialize]
-def mfirst {m : Type u → Type v} [Monad m] [Alternative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m β
+def firstM {m : Type u → Type v} [Monad m] [Alternative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m β
 | []    => failure
-| a::as => f a <|> mfirst as
+| a::as => f a <|> firstM as
 
 @[specialize]
-def mexists {m : Type → Type u} [Monad m] {α : Type v} (f : α → m Bool) : List α → m Bool
+def anyM {m : Type → Type u} [Monad m] {α : Type v} (f : α → m Bool) : List α → m Bool
 | []    => pure false
 | a::as => do b ← f a; match b with
   | true  => pure true
-  | false =>  mexists as
+  | false =>  anyM as
 
 @[specialize]
-def mforall {m : Type → Type u} [Monad m] {α : Type v} (f : α → m Bool) : List α → m Bool
+def allM {m : Type → Type u} [Monad m] {α : Type v} (f : α → m Bool) : List α → m Bool
 | []    => pure true
 | a::as => do b ← f a; match b with
-  | true  => mforall as
+  | true  => allM as
   | false => pure false
 
 end List
diff --git a/library/Init/Data/Array/Basic.lean b/library/Init/Data/Array/Basic.lean
index f91c0eb8c3..124f244d22 100644
--- a/library/Init/Data/Array/Basic.lean
+++ b/library/Init/Data/Array/Basic.lean
@@ -156,55 +156,54 @@ variables {m : Type v → Type w} [Monad m]
 variables {β : Type v} {σ : Type u}
 
 -- TODO(Leo): justify termination using wf-rec
-@[specialize] partial def miterateAux (a : Array α) (f : ∀ (i : Fin a.size), α → β → m β) : Nat → β → m β
+@[specialize] partial def iterateMAux (a : Array α) (f : ∀ (i : Fin a.size), α → β → m β) : Nat → β → m β
 | i, b =>
   if h : i < a.size then
      let idx : Fin a.size := ⟨i, h⟩;
-     f idx (a.get idx) b >>= miterateAux (i+1)
+     f idx (a.get idx) b >>= iterateMAux (i+1)
   else pure b
 
-@[inline] def miterate (a : Array α) (b : β) (f : ∀ (i : Fin a.size), α → β → m β) : m β :=
-miterateAux a f 0 b
+@[inline] def iterateM (a : Array α) (b : β) (f : ∀ (i : Fin a.size), α → β → m β) : m β :=
+iterateMAux a f 0 b
 
-@[inline] def mfoldl (f : β → α → m β) (b : β) (a : Array α) : m β :=
-miterate a b (fun _ b a => f a b)
+@[inline] def foldlM (f : β → α → m β) (b : β) (a : Array α) : m β :=
+iterateM a b (fun _ b a => f a b)
 
-@[inline] def mfoldlFrom (f : β → α → m β) (b : β) (a : Array α) (ini : Nat := 0) : m β :=
-miterateAux a (fun _ b a => f a b) ini b
+@[inline] def foldlFromM (f : β → α → m β) (b : β) (a : Array α) (ini : Nat := 0) : m β :=
+iterateMAux a (fun _ b a => f a b) ini b
 
 -- TODO(Leo): justify termination using wf-rec
-@[specialize] partial def miterate₂Aux (a₁ : Array α) (a₂ : Array σ) (f : ∀ (i : Fin a₁.size), α → σ → β → m β) : Nat → β → m β
+@[specialize] partial def iterateM₂Aux (a₁ : Array α) (a₂ : Array σ) (f : ∀ (i : Fin a₁.size), α → σ → β → m β) : Nat → β → m β
 | i, b =>
   if h₁ : i < a₁.size then
      let idx₁ : Fin a₁.size := ⟨i, h₁⟩;
      if h₂ : i < a₂.size then
        let idx₂ : Fin a₂.size := ⟨i, h₂⟩;
-       f idx₁ (a₁.get idx₁) (a₂.get idx₂) b >>= miterate₂Aux (i+1)
+       f idx₁ (a₁.get idx₁) (a₂.get idx₂) b >>= iterateM₂Aux (i+1)
      else pure b
   else pure b
 
-@[inline] def miterate₂ (a₁ : Array α) (a₂ : Array σ) (b : β) (f : ∀ (i : Fin a₁.size), α → σ → β → m β) : m β :=
-miterate₂Aux a₁ a₂ f 0 b
-
-@[inline] def mfoldl₂ (f : β → α → σ → m β) (b : β) (a₁ : Array α) (a₂ : Array σ): m β :=
-miterate₂ a₁ a₂ b (fun _ a₁ a₂ b => f b a₁ a₂)
+@[inline] def iterateM₂ (a₁ : Array α) (a₂ : Array σ) (b : β) (f : ∀ (i : Fin a₁.size), α → σ → β → m β) : m β :=
+iterateM₂Aux a₁ a₂ f 0 b
 
+@[inline] def foldlM₂ (f : β → α → σ → m β) (b : β) (a₁ : Array α) (a₂ : Array σ): m β :=
+iterateM₂ a₁ a₂ b (fun _ a₁ a₂ b => f b a₁ a₂)
 
 -- TODO(Leo): justify termination using wf-rec
-@[specialize] partial def mfindAux (a : Array α) (f : α → m (Option β)) : Nat → m (Option β)
+@[specialize] partial def findMAux (a : Array α) (f : α → m (Option β)) : Nat → m (Option β)
 | i =>
   if h : i < a.size then
      let idx : Fin a.size := ⟨i, h⟩;
      do r ← f (a.get idx);
         match r with
         | some v => pure r
-        | none   => mfindAux (i+1)
+        | none   => findMAux (i+1)
   else pure none
 
-@[inline] def mfind (a : Array α) (f : α → m (Option β)) : m (Option β) :=
-mfindAux a f 0
+@[inline] def findM (a : Array α) (f : α → m (Option β)) : m (Option β) :=
+findMAux a f 0
 
-@[specialize] partial def mfindRevAux (a : Array α) (f : α → m (Option β)) : ∀ (idx : Nat), idx ≤ a.size → m (Option β)
+@[specialize] partial def findRevMAux (a : Array α) (f : α → m (Option β)) : ∀ (idx : Nat), idx ≤ a.size → m (Option β)
 | i, h =>
   if hLt : 0 < i then
     have i - 1 < i from Nat.subLt hLt (Nat.zeroLtSucc 0);
@@ -216,11 +215,11 @@ mfindAux a f 0
       | some v => pure r
       | none   =>
         have i - 1 ≤ a.size from Nat.leOfLt this;
-        mfindRevAux (i-1) this
+        findRevMAux (i-1) this
   else pure none
 
-@[inline] def mfindRev (a : Array α) (f : α → m (Option β)) : m (Option β) :=
-mfindRevAux a f a.size (Nat.leRefl _)
+@[inline] def findRevM (a : Array α) (f : α → m (Option β)) : m (Option β) :=
+findRevMAux a f a.size (Nat.leRefl _)
 
 end
 
@@ -228,25 +227,25 @@ section
 variables {β : Type w} {σ : Type u}
 
 @[inline] def iterate (a : Array α) (b : β) (f : ∀ (i : Fin a.size), α → β → β) : β :=
-Id.run $ miterateAux a f 0 b
+Id.run $ iterateMAux a f 0 b
 
 @[inline] def iterateFrom (a : Array α) (b : β) (i : Nat) (f : ∀ (i : Fin a.size), α → β → β) : β :=
-Id.run $ miterateAux a f i b
+Id.run $ iterateMAux a f i b
 
 @[inline] def foldl (f : β → α → β) (b : β) (a : Array α) : β :=
 iterate a b (fun _ a b => f b a)
 
 @[inline] def foldlFrom (f : β → α → β) (b : β) (a : Array α) (ini : Nat := 0) : β :=
-Id.run $ mfoldlFrom f b a ini
+Id.run $ foldlFromM f b a ini
 
 @[inline] def iterate₂ (a₁ : Array α) (a₂ : Array σ) (b : β) (f : ∀ (i : Fin a₁.size), α → σ → β → β) : β :=
-Id.run $ miterate₂Aux a₁ a₂ f 0 b
+Id.run $ iterateM₂Aux a₁ a₂ f 0 b
 
 @[inline] def foldl₂ (f : β → α → σ → β) (b : β) (a₁ : Array α) (a₂ : Array σ) : β :=
 iterate₂ a₁ a₂ b (fun _ a₁ a₂ b => f b a₁ a₂)
 
 @[inline] def find? (a : Array α) (f : α → Option β) : Option β :=
-Id.run $ mfindAux a f 0
+Id.run $ findMAux a f 0
 
 @[inline] def find! [Inhabited β] (a : Array α) (f : α → Option β) : β :=
 match find? a f with
@@ -254,7 +253,7 @@ match find? a f with
 | none   => panic! "failed to find element"
 
 @[inline] def findRev? (a : Array α) (f : α → Option β) : Option β :=
-Id.run $ mfindRevAux a f a.size (Nat.leRefl _)
+Id.run $ findRevMAux a f a.size (Nat.leRefl _)
 
 @[inline] def findRev! [Inhabited β] (a : Array α) (f : α → Option β) : β :=
 match findRev? a f with
@@ -309,26 +308,26 @@ section
 variables {m : Type v → Type w} [Monad m]
 variable {β : Type v}
 
-@[specialize] private def miterateRevAux (a : Array α) (f : ∀ (i : Fin a.size), α → β → m β) : ∀ (i : Nat), i ≤ a.size → β → m β
+@[specialize] private def iterateRevMAux (a : Array α) (f : ∀ (i : Fin a.size), α → β → m β) : ∀ (i : Nat), i ≤ a.size → β → m β
 | 0,   h, b => pure b
 | j+1, h, b => do
   let i : Fin a.size := ⟨j, h⟩;
   b ← f i (a.get i) b;
-  miterateRevAux j (Nat.leOfLt h) b
+  iterateRevMAux j (Nat.leOfLt h) b
 
-@[inline] def miterateRev (a : Array α) (b : β) (f : ∀ (i : Fin a.size), α → β → m β) : m β :=
-miterateRevAux a f a.size (Nat.leRefl _) b
+@[inline] def iterateRevM (a : Array α) (b : β) (f : ∀ (i : Fin a.size), α → β → m β) : m β :=
+iterateRevMAux a f a.size (Nat.leRefl _) b
 
-@[inline] def mfoldr (f : α → β → m β) (b : β) (a : Array α) : m β :=
-miterateRev a b (fun _ => f)
+@[inline] def foldrM (f : α → β → m β) (b : β) (a : Array α) : m β :=
+iterateRevM a b (fun _ => f)
 
 end
 
 @[inline] def iterateRev {β} (a : Array α) (b : β) (f : ∀ (i : Fin a.size), α → β → β) : β :=
-Id.run $ miterateRev a b f
+Id.run $ iterateRevM a b f
 
 @[inline] def foldr {β} (f : α → β → β) (b : β) (a : Array α) : β :=
-Id.run $ mfoldr f b a
+Id.run $ foldrM f b a
 
 def toList (a : Array α) : List α :=
 a.foldr List.cons []
@@ -343,27 +342,27 @@ section
 variables {m : Type u → Type w} [Monad m]
 variable {β : Type u}
 
-@[specialize] unsafe partial def ummapAux (f : Nat → α → m β) : Nat → Array α → m (Array β)
+@[specialize] unsafe partial def umapMAux (f : Nat → α → m β) : Nat → Array α → m (Array β)
 | i, a =>
   if h : i < a.size then
      let idx : Fin a.size := ⟨i, h⟩;
      let v   : α          := a.get idx;
      let a                := a.set idx (@unsafeCast _ _ ⟨v⟩ ());
-     do newV ← f i v; ummapAux (i+1) (a.set idx (@unsafeCast _ _ ⟨v⟩ newV))
+     do newV ← f i v; umapMAux (i+1) (a.set idx (@unsafeCast _ _ ⟨v⟩ newV))
   else
      pure (unsafeCast a)
 
-@[inline] unsafe partial def ummap (f : α → m β) (as : Array α) : m (Array β) :=
-ummapAux (fun i a => f a) 0 as
+@[inline] unsafe partial def umapM (f : α → m β) (as : Array α) : m (Array β) :=
+umapMAux (fun i a => f a) 0 as
 
-@[inline] unsafe partial def ummapIdx (f : Nat → α → m β) (as : Array α) : m (Array β) :=
-ummapAux f 0 as
+@[inline] unsafe partial def umapIdxM (f : Nat → α → m β) (as : Array α) : m (Array β) :=
+umapMAux f 0 as
 
-@[implementedBy Array.ummap] def mmap (f : α → m β) (as : Array α) : m (Array β) :=
-as.mfoldl (fun bs a => do b ← f a; pure (bs.push b)) (mkEmpty as.size)
+@[implementedBy Array.umapM] def mapM (f : α → m β) (as : Array α) : m (Array β) :=
+as.foldlM (fun bs a => do b ← f a; pure (bs.push b)) (mkEmpty as.size)
 
-@[implementedBy Array.ummapIdx] def mmapIdx (f : Nat → α → m β) (as : Array α) : m (Array β) :=
-as.miterate (mkEmpty as.size) (fun i a bs => do b ← f i.val a; pure (bs.push b))
+@[implementedBy Array.umapIdxM] def mapIdxM (f : Nat → α → m β) (as : Array α) : m (Array β) :=
+as.iterateM (mkEmpty as.size) (fun i a bs => do b ← f i.val a; pure (bs.push b))
 end
 
 section
@@ -380,10 +379,10 @@ else
   a
 
 @[inline] def mapIdx (f : Nat → α → β) (a : Array α) : Array β :=
-Id.run $ mmapIdx f a
+Id.run $ mapIdxM f a
 
 @[inline] def map (f : α → β) (as : Array α) : Array β :=
-Id.run $ mmap f as
+Id.run $ mapM f as
 end
 
 section
@@ -391,17 +390,17 @@ variables {m : Type u → Type v} [Monad m]
 variable {β : Type u}
 
 @[specialize]
-partial def mforAux {α : Type w} {β : Type u} (f : α → m β) (a : Array α) : Nat → m PUnit
+partial def forMAux {α : 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⟩;
      let v   : α          := a.get idx;
-     f v *> mforAux (i+1)
+     f v *> forMAux (i+1)
   else
      pure ⟨⟩
 
-def mfor {α : Type w} {β : Type u} (f : α → m β) (a : Array α) : m PUnit :=
-a.mforAux f 0
+def forM {α : Type w} {β : Type u} (f : α → m β) (a : Array α) : m PUnit :=
+a.forMAux f 0
 
 end
 
diff --git a/library/Init/Data/AssocList.lean b/library/Init/Data/AssocList.lean
index 4565ce0322..220c1f4246 100644
--- a/library/Init/Data/AssocList.lean
+++ b/library/Init/Data/AssocList.lean
@@ -18,12 +18,12 @@ variables {α : Type u} {β : Type v} {δ : Type w} {m : Type w → Type w} [Mon
 def empty : AssocList α β :=
 nil
 
-@[specialize] def mfoldl (f : δ → α → β → m δ) : δ → AssocList α β → m δ
+@[specialize] def foldlM (f : δ → α → β → m δ) : δ → AssocList α β → m δ
 | d, nil         => pure d
-| d, cons a b es => do d ← f d a b; mfoldl d es
+| d, cons a b es => do d ← f d a b; foldlM d es
 
 @[inline] def foldl (f : δ → α → β → δ) (d : δ) (as : AssocList α β) : δ :=
-Id.run (mfoldl f d as)
+Id.run (foldlM f d as)
 
 def find [HasBeq α] (a : α) : AssocList α β → Option β
 | nil         => none
diff --git a/library/Init/Data/HashMap/Basic.lean b/library/Init/Data/HashMap/Basic.lean
index fd80061656..67937ffd84 100644
--- a/library/Init/Data/HashMap/Basic.lean
+++ b/library/Init/Data/HashMap/Basic.lean
@@ -44,14 +44,14 @@ def mkIdx {n : Nat} (h : n > 0) (u : USize) : { u : USize // u.toNat < n } :=
 let ⟨i, h⟩ := mkIdx data.property (hashFn a);
 data.update i (AssocList.cons a b (data.val.uget i h)) h
 
-@[inline] def mfoldBuckets {δ : Type w} {m : Type w → Type w} [Monad m] (data : HashMapBucket α β) (d : δ) (f : δ → α → β → m δ) : m δ :=
-data.val.mfoldl (fun d b => b.mfoldl f d) d
+@[inline] def foldBucketsM {δ : Type w} {m : Type w → Type w} [Monad m] (data : HashMapBucket α β) (d : δ) (f : δ → α → β → m δ) : m δ :=
+data.val.foldlM (fun d b => b.foldlM f d) d
 
 @[inline] def foldBuckets {δ : Type w} (data : HashMapBucket α β) (d : δ) (f : δ → α → β → δ) : δ :=
-Id.run $ mfoldBuckets data d f
+Id.run $ foldBucketsM data d f
 
-@[inline] def mfold {δ : Type w} {m : Type w → Type w} [Monad m] (f : δ → α → β → m δ) (d : δ) (h : HashMapImp α β) : m δ :=
-mfoldBuckets h.buckets d f
+@[inline] def foldM {δ : Type w} {m : Type w → Type w} [Monad m] (f : δ → α → β → m δ) (d : δ) (h : HashMapImp α β) : m δ :=
+foldBucketsM h.buckets d f
 
 @[inline] def fold {δ : Type w} (f : δ → α → β → δ) (d : δ) (m : HashMapImp α β) : δ :=
 foldBuckets m.buckets d f
@@ -158,9 +158,9 @@ match m.find a with
 match m with
 | ⟨ m, _ ⟩ => m.contains a
 
-@[inline] def mfold {δ : Type w} {m : Type w → Type w} [Monad m] (f : δ → α → β → m δ) (d : δ) (h : HashMap α β) : m δ :=
+@[inline] def foldM {δ : Type w} {m : Type w → Type w} [Monad m] (f : δ → α → β → m δ) (d : δ) (h : HashMap α β) : m δ :=
 match h with
-| ⟨ h, _ ⟩ => h.mfold f d
+| ⟨ h, _ ⟩ => h.foldM f d
 
 @[inline] def fold {δ : Type w} (f : δ → α → β → δ) (d : δ) (m : HashMap α β) : δ :=
 match m with
diff --git a/library/Init/Data/HashSet.lean b/library/Init/Data/HashSet.lean
index 60bd0d8db7..30be96338e 100644
--- a/library/Init/Data/HashSet.lean
+++ b/library/Init/Data/HashSet.lean
@@ -42,10 +42,10 @@ s.set.isEmpty
 @[inline] def empty : HashSet α :=
 mkHashSet
 
-@[inline] def mfold {β : Type v} {m : Type v → Type v} [Monad m] (f : β → α → m β) (d : β) (s : HashSet α) : m β :=
-s.set.mfold (fun d a _ => f d a) d
+@[inline] def foldM {β : Type v} {m : Type v → Type v} [Monad m] (f : β → α → m β) (d : β) (s : HashSet α) : m β :=
+s.set.foldM (fun d a _ => f d a) d
 
 @[inline] def fold {β : Type v} (f : β → α → β) (d : β) (s : HashSet α) : β :=
-Id.run $ s.mfold f d
+Id.run $ s.foldM f d
 
 end HashSet
diff --git a/library/Init/Data/PersistentArray/Basic.lean b/library/Init/Data/PersistentArray/Basic.lean
index a218747172..ec12d6f74c 100644
--- a/library/Init/Data/PersistentArray/Basic.lean
+++ b/library/Init/Data/PersistentArray/Basic.lean
@@ -187,67 +187,67 @@ section
 variables {m : Type v → Type w} [Monad m]
 variable {β : Type v}
 
-@[specialize] partial def mfoldlAux (f : β → α → m β) : PersistentArrayNode α → β → m β
-| node cs, b => cs.mfoldl (fun b c => mfoldlAux c b) b
-| leaf vs, b => vs.mfoldl f b
+@[specialize] partial def foldlMAux (f : β → α → m β) : PersistentArrayNode α → β → m β
+| node cs, b => cs.foldlM (fun b c => foldlMAux c b) b
+| leaf vs, b => vs.foldlM f b
 
-@[specialize] def mfoldl (t : PersistentArray α) (f : β → α → m β) (b : β) : m β :=
-do b ← mfoldlAux f t.root b; t.tail.mfoldl f b
+@[specialize] def foldlM (t : PersistentArray α) (f : β → α → m β) (b : β) : m β :=
+do b ← foldlMAux f t.root b; t.tail.foldlM f b
 
-@[specialize] partial def mfindAux (f : α → m (Option β)) : PersistentArrayNode α → m (Option β)
-| node cs => cs.mfind (fun c => mfindAux c)
-| leaf vs => vs.mfind f
+@[specialize] partial def findMAux (f : α → m (Option β)) : PersistentArrayNode α → m (Option β)
+| node cs => cs.findM (fun c => findMAux c)
+| leaf vs => vs.findM f
 
-@[specialize] def mfind (t : PersistentArray α) (f : α → m (Option β)) : m (Option β) :=
-do b ← mfindAux f t.root;
+@[specialize] def findM (t : PersistentArray α) (f : α → m (Option β)) : m (Option β) :=
+do b ← findMAux f t.root;
    match b with
-   | none   => t.tail.mfind f
+   | none   => t.tail.findM f
    | some b => pure (some b)
 
-@[specialize] partial def mfindRevAux (f : α → m (Option β)) : PersistentArrayNode α → m (Option β)
-| node cs => cs.mfindRev (fun c => mfindRevAux c)
-| leaf vs => vs.mfindRev f
+@[specialize] partial def findRevMAux (f : α → m (Option β)) : PersistentArrayNode α → m (Option β)
+| node cs => cs.findRevM (fun c => findRevMAux c)
+| leaf vs => vs.findRevM f
 
-@[specialize] def mfindRev (t : PersistentArray α) (f : α → m (Option β)) : m (Option β) :=
-do b ← t.tail.mfindRev f;
+@[specialize] def findRevM (t : PersistentArray α) (f : α → m (Option β)) : m (Option β) :=
+do b ← t.tail.findRevM f;
    match b with
-   | none   => mfindRevAux f t.root
+   | none   => findRevMAux f t.root
    | some b => pure (some b)
 
-partial def mfoldlFromAux (f : β → α → m β) : PersistentArrayNode α → USize → USize → β → m β
+partial def foldlFromMAux (f : β → α → m β) : PersistentArrayNode α → USize → USize → β → m β
 | node cs, i, shift, b => do
   let j    := (div2Shift i shift).toNat;
-  b ← mfoldlFromAux (cs.get! j) (mod2Shift i shift) (shift - initShift) b;
-  cs.mfoldlFrom (fun b c => mfoldlAux f c b) b (j+1)
-| leaf vs, i, _, b => vs.mfoldlFrom f b i.toNat
+  b ← foldlFromMAux (cs.get! j) (mod2Shift i shift) (shift - initShift) b;
+  cs.foldlFromM (fun b c => foldlMAux f c b) b (j+1)
+| leaf vs, i, _, b => vs.foldlFromM f b i.toNat
 
-def mfoldlFrom (t : PersistentArray α) (f : β → α → m β) (b : β) (ini : Nat) : m β :=
+def foldlFromM (t : PersistentArray α) (f : β → α → m β) (b : β) (ini : Nat) : m β :=
 if ini >= t.tailOff then
-  t.tail.mfoldlFrom f b (ini - t.tailOff)
+  t.tail.foldlFromM f b (ini - t.tailOff)
 else do
-  b ← mfoldlFromAux f t.root (USize.ofNat ini) t.shift b;
-  t.tail.mfoldl f b
+  b ← foldlFromMAux f t.root (USize.ofNat ini) t.shift b;
+  t.tail.foldlM f b
 
-@[specialize] partial def mforAux (f : α → m β) : PersistentArrayNode α → m PUnit
-| node cs => cs.mfor (fun c => mforAux c)
-| leaf vs => vs.mfor f
+@[specialize] partial def forMAux (f : α → m β) : PersistentArrayNode α → m PUnit
+| node cs => cs.forM (fun c => forMAux c)
+| leaf vs => vs.forM f
 
-@[specialize] def mfor (t : PersistentArray α) (f : α → m β) : m PUnit :=
-mforAux f t.root *> t.tail.mfor f
+@[specialize] def forM (t : PersistentArray α) (f : α → m β) : m PUnit :=
+forMAux f t.root *> t.tail.forM f
 
 end
 
 @[inline] def foldl {β} (t : PersistentArray α) (f : β → α → β) (b : β) : β :=
-Id.run (t.mfoldl f b)
+Id.run (t.foldlM f b)
 
 @[inline] def find {β} (t : PersistentArray α) (f : α → (Option β)) : Option β :=
-Id.run (t.mfind f)
+Id.run (t.findM f)
 
 @[inline] def findRev {β} (t : PersistentArray α) (f : α → (Option β)) : Option β :=
-Id.run (t.mfindRev f)
+Id.run (t.findRevM f)
 
 @[inline] def foldlFrom {β} (t : PersistentArray α) (f : β → α → β) (b : β) (ini : Nat) : β :=
-Id.run (t.mfoldlFrom f b ini)
+Id.run (t.foldlFromM f b ini)
 
 def toList (t : PersistentArray α) : List α :=
 (t.foldl (fun xs x => x :: xs) []).reverse
@@ -276,19 +276,19 @@ section
 variables {m : Type u → Type v} [Monad m]
 variable {β : Type u}
 
-@[specialize] partial def mmapAux (f : α → m β) : PersistentArrayNode α → m (PersistentArrayNode β)
-| node cs => node <$> cs.mmap (fun c => mmapAux c)
-| leaf vs => leaf <$> vs.mmap f
+@[specialize] partial def mapMAux (f : α → m β) : PersistentArrayNode α → m (PersistentArrayNode β)
+| node cs => node <$> cs.mapM (fun c => mapMAux c)
+| leaf vs => leaf <$> vs.mapM f
 
-@[specialize] def mmap (f : α → m β) (t : PersistentArray α) : m (PersistentArray β) :=
-do root ← mmapAux f t.root;
-   tail ← t.tail.mmap f;
+@[specialize] def mapM (f : α → m β) (t : PersistentArray α) : m (PersistentArray β) :=
+do root ← mapMAux f t.root;
+   tail ← t.tail.mapM f;
    pure { tail := tail, root := root, .. t }
 
 end
 
 @[inline] def map {β} (f : α → β) (t : PersistentArray α) : PersistentArray β :=
-Id.run (t.mmap f)
+Id.run (t.mapM f)
 
 structure Stats :=
 (numNodes : Nat) (depth : Nat) (tailSize : Nat)
diff --git a/library/Init/Data/PersistentHashMap/Basic.lean b/library/Init/Data/PersistentHashMap/Basic.lean
index 2f10174a72..276172c04a 100644
--- a/library/Init/Data/PersistentHashMap/Basic.lean
+++ b/library/Init/Data/PersistentHashMap/Basic.lean
@@ -238,20 +238,20 @@ section
 variables {m : Type w → Type w'} [Monad m]
 variables {σ : Type w}
 
-@[specialize] partial def mfoldlAux (f : σ → α → β → m σ) : Node α β → σ → m σ
-| Node.collision keys vals heq, acc => keys.miterate acc $ fun i k acc => f acc k (vals.get ⟨i.val, heq ▸ i.isLt⟩)
-| Node.entries entries, acc => entries.mfoldl (fun acc entry =>
+@[specialize] partial def foldlMAux (f : σ → α → β → m σ) : Node α β → σ → m σ
+| Node.collision keys vals heq, acc => keys.iterateM acc $ fun i k acc => f acc k (vals.get ⟨i.val, heq ▸ i.isLt⟩)
+| Node.entries entries, acc => entries.foldlM (fun acc entry =>
   match entry with
   | Entry.null      => pure acc
   | Entry.entry k v => f acc k v
-  | Entry.ref node  => mfoldlAux node acc)
+  | Entry.ref node  => foldlMAux node acc)
   acc
 
-@[specialize] def mfoldl (map : PersistentHashMap α β) (f : σ → α → β → m σ) (acc : σ) : m σ :=
-mfoldlAux f map.root acc
+@[specialize] def foldlM (map : PersistentHashMap α β) (f : σ → α → β → m σ) (acc : σ) : m σ :=
+foldlMAux f map.root acc
 
 @[specialize] def foldl (map : PersistentHashMap α β) (f : σ → α → β → σ) (acc : σ) : σ :=
-Id.run $ map.mfoldl f acc
+Id.run $ map.foldlM f acc
 end
 
 def toList (m : PersistentHashMap α β) : List (α × β) :=
diff --git a/library/Init/Data/PersistentHashSet.lean b/library/Init/Data/PersistentHashSet.lean
index 7ca6acc249..9a63be93b6 100644
--- a/library/Init/Data/PersistentHashSet.lean
+++ b/library/Init/Data/PersistentHashSet.lean
@@ -41,10 +41,10 @@ s.set.contains a
 @[inline] def size (s : PersistentHashSet α) : Nat :=
 s.set.size
 
-@[inline] def mfold {β : Type v} {m : Type v → Type v} [Monad m] (f : β → α → m β) (d : β) (s : PersistentHashSet α) : m β :=
-s.set.mfoldl (fun d a _ => f d a) d
+@[inline] def foldM {β : Type v} {m : Type v → Type v} [Monad m] (f : β → α → m β) (d : β) (s : PersistentHashSet α) : m β :=
+s.set.foldlM (fun d a _ => f d a) d
 
 @[inline] def fold {β : Type v} (f : β → α → β) (d : β) (s : PersistentHashSet α) : β :=
-Id.run $ s.mfold f d
+Id.run $ s.foldM f d
 
 end PersistentHashSet
diff --git a/library/Init/Lean/AbstractMetavarContext.lean b/library/Init/Lean/AbstractMetavarContext.lean
index 538d3c7985..cc0bc61166 100644
--- a/library/Init/Lean/AbstractMetavarContext.lean
+++ b/library/Init/Lean/AbstractMetavarContext.lean
@@ -234,7 +234,7 @@ partial def main : Expr → M σ Expr
 | e@(Expr.forallE _ _ d b) => do d ← visit main d; b ← visit main b; pure (e.updateForallE! d b)
 | e@(Expr.lam _ _ d b)     => do d ← visit main d; b ← visit main b; pure (e.updateLambdaE! d b)
 | e@(Expr.letE _ t v b)    => do t ← visit main t; v ← visit main v; b ← visit main b; pure (e.updateLet! t v b)
-| e@(Expr.const _ lvls)    => do lvls ← lvls.mmap instantiateLevelMVars; pure (e.updateConst! lvls)
+| e@(Expr.const _ lvls)    => do lvls ← lvls.mapM instantiateLevelMVars; pure (e.updateConst! lvls)
 | e@(Expr.sort lvl)        => do lvl ← instantiateLevelMVars lvl; pure (e.updateSort! lvl)
 | e@(Expr.mdata _ b)       => do b ← visit main b; pure (e.updateMData! b)
 | e@(Expr.app _ _)         => e.withAppRev $ fun f revArgs => do
@@ -244,7 +244,7 @@ partial def main : Expr → M σ Expr
     -- Some of the arguments in revArgs are irrelevant after we beta reduce.
     visit main (f.betaRev revArgs)
   else do
-    revArgs ← revArgs.mmap (visit main);
+    revArgs ← revArgs.mapM (visit main);
     pure (mkAppRev f revArgs)
 | e@(Expr.mvar mvarId)     => checkCache e $ fun e => do
   mctx ← getMCtx;
diff --git a/library/Init/Lean/Attributes.lean b/library/Init/Lean/Attributes.lean
index 47a8ef8e47..d69e4b8e3a 100644
--- a/library/Init/Lean/Attributes.lean
+++ b/library/Init/Lean/Attributes.lean
@@ -115,7 +115,7 @@ do attr ← getAttributeImpl attrName;
 @[export lean_activate_scoped_attributes]
 def activateScopedAttributes (env : Environment) (scope : Name) : IO Environment :=
 do attrs ← attributeArrayRef.get;
-   attrs.mfoldl (fun env attr => attr.activateScoped env scope) env
+   attrs.foldlM (fun env attr => attr.activateScoped env scope) env
 
 /- We use this function to implement commands `namespace foo` and `section foo`.
    It activates scoped attributes in the new resulting namespace. -/
@@ -124,14 +124,14 @@ def pushScope (env : Environment) (header : Name) (isNamespace : Bool) : IO Envi
 do let env := env.pushScopeCore header isNamespace;
    let ns  := env.getNamespace;
    attrs ← attributeArrayRef.get;
-   attrs.mfoldl (fun env attr => do env ← attr.pushScope env; if isNamespace then attr.activateScoped env ns else pure env) env
+   attrs.foldlM (fun env attr => do env ← attr.pushScope env; if isNamespace then attr.activateScoped env ns else pure env) env
 
 /- We use this function to implement commands `end foo` for closing namespaces and sections. -/
 @[export lean_pop_scope]
 def popScope (env : Environment) : IO Environment :=
 do let env := env.popScopeCore;
    attrs ← attributeArrayRef.get;
-   attrs.mfoldl (fun env attr => attr.popScope env) env
+   attrs.foldlM (fun env attr => attr.popScope env) env
 
 end Environment
 
@@ -274,7 +274,7 @@ do ext : PersistentEnvExtension (Name × α) (NameMap α) ← registerPersistent
        | Except.error msg => throw (IO.userError ("invalid attribute '" ++ toString name ++ "', " ++ msg))
        | _                => pure $ ext.addEntry env (decl, val)
    };
-   attrs.mfor registerAttribute;
+   attrs.forM registerAttribute;
    pure { ext := ext, attrs := attrs }
 
 namespace EnumAttributes
diff --git a/library/Init/Lean/Compiler/IR/Basic.lean b/library/Init/Lean/Compiler/IR/Basic.lean
index 9bb612715f..2ddfc8f075 100644
--- a/library/Init/Lean/Compiler/IR/Basic.lean
+++ b/library/Init/Lean/Compiler/IR/Basic.lean
@@ -389,7 +389,7 @@ bs.map $ fun b => match b with
   | other                 => other
 
 @[inline] def mmodifyJPs {m : Type → Type} [Monad m] (bs : Array FnBody) (f : FnBody → m FnBody) : m (Array FnBody) :=
-bs.mmap $ fun b => match b with
+bs.mapM $ fun b => match b with
   | FnBody.jdecl j xs v k => do v ← f v; pure $ FnBody.jdecl j xs v k
   | other                 => pure other
 
diff --git a/library/Init/Lean/Compiler/IR/Borrow.lean b/library/Init/Lean/Compiler/IR/Borrow.lean
index 0797b58d94..f2cae7c76e 100644
--- a/library/Init/Lean/Compiler/IR/Borrow.lean
+++ b/library/Init/Lean/Compiler/IR/Borrow.lean
@@ -79,7 +79,7 @@ partial def visitFnBody (fnid : FunId) : FnBody → State ParamMap Unit
     visitFnBody b
 
 def visitDecls (env : Environment) (decls : Array Decl) : State ParamMap Unit :=
-decls.mfor $ fun decl => match decl with
+decls.forM $ fun decl => match decl with
   | Decl.fdecl f xs _ b => do
     let exported := isExport env f;
     modify $ fun m => m.insert (Key.decl f) (initBorrowIfNotExported exported xs);
@@ -153,7 +153,7 @@ match x with
 | _           => pure ()
 
 def ownArgs (xs : Array Arg) : M Unit :=
-xs.mfor ownArg
+xs.forM ownArg
 
 def isOwned (x : VarId) : M Bool :=
 do s ← get;
@@ -164,7 +164,7 @@ def updateParamMap (k : Key) : M Unit :=
 do s ← get;
    match s.map.find k with
    | some ps => do
-     ps ← ps.mmap $ fun (p : Param) =>
+     ps ← ps.mapM $ fun (p : Param) =>
       if p.borrow && s.owned.contains p.x.idx then do
         markModifiedParamMap; pure { borrow := false, .. p }
       else
@@ -187,7 +187,7 @@ do s ← get;
 
 /- For each ps[i], if ps[i] is owned, then mark xs[i] as owned. -/
 def ownArgsUsingParams (xs : Array Arg) (ps : Array Param) : M Unit :=
-xs.size.mfor $ fun i => do
+xs.size.forM $ fun i => do
   let x := xs.get! i;
   let p := ps.get! i;
   unless p.borrow $ ownArg x
@@ -198,11 +198,11 @@ xs.size.mfor $ fun i => do
    we would have to insert a `dec xs[i]` after `f xs` and consequently
    "break" the tail call. -/
 def ownParamsUsingArgs (xs : Array Arg) (ps : Array Param) : M Unit :=
-xs.size.mfor $ fun i => do
+xs.size.forM $ fun i => do
   let x := xs.get! i;
   let p := ps.get! i;
   match x with
-  | Arg.var x => mwhen (isOwned x) $ ownVar p.x
+  | Arg.var x => whenM (isOwned x) $ ownVar p.x
   | _         => pure ()
 
 /- Mark `xs[i]` as owned if it is one of the parameters `ps`.
@@ -217,7 +217,7 @@ xs.size.mfor $ fun i => do
 -/
 def ownArgsIfParam (xs : Array Arg) : M Unit :=
 do ctx ← read;
-   xs.mfor $ fun x =>
+   xs.forM $ fun x =>
      match x with
      | Arg.var x => when (ctx.paramSet.contains x.idx) $ ownVar x
      | _ => pure ()
@@ -226,7 +226,7 @@ def collectExpr (z : VarId) : Expr → M Unit
 | Expr.reset _ x      => ownVar z *> ownVar x
 | Expr.reuse x _ _ ys => ownVar z *> ownVar x *> ownArgsIfParam ys
 | Expr.ctor _ xs      => ownVar z *> ownArgsIfParam xs
-| Expr.proj _ x       => mwhen (isOwned z) $ ownVar x
+| Expr.proj _ x       => whenM (isOwned z) $ ownVar x
 | Expr.fap g xs       => do ps ← getParamInfo (Key.decl g);
   -- dbgTrace ("collectExpr: " ++ toString g ++ " " ++ toString (formatParams ps)) $ fun _ =>
   ownVar z *> ownArgsUsingParams xs ps
@@ -259,7 +259,7 @@ partial def collectFnBody : FnBody → M Unit
   ps ← getParamInfo (Key.jp ctx.currFn j);
   ownArgsUsingParams ys ps; -- for making sure the join point can reuse
   ownParamsUsingArgs ys ps  -- for making sure the tail call is preserved
-| FnBody.case _ _ _ alts => alts.mfor $ fun alt => collectFnBody alt.body
+| FnBody.case _ _ _ alts => alts.forM $ fun alt => collectFnBody alt.body
 | e                      => unless (e.isTerminal) $ collectFnBody e.body
 
 @[specialize] partial def whileModifingOwnedAux (x : M Unit) : Unit → M Unit
@@ -297,7 +297,7 @@ partial def collectDecl : Decl → M Unit
 whileModifingParamMapAux x ()
 
 def collectDecls (decls : Array Decl) : M ParamMap :=
-do whileModifingParamMap (decls.mfor collectDecl);
+do whileModifingParamMap (decls.forM collectDecl);
    s ← get;
    pure s.map
 
diff --git a/library/Init/Lean/Compiler/IR/Boxing.lean b/library/Init/Lean/Compiler/IR/Boxing.lean
index cde509269f..252eec94a0 100644
--- a/library/Init/Lean/Compiler/IR/Boxing.lean
+++ b/library/Init/Lean/Compiler/IR/Boxing.lean
@@ -52,8 +52,8 @@ let ps := decl.params;
 
 def mkBoxedVersionAux (decl : Decl) : N Decl :=
 do let ps := decl.params;
-   qs ← ps.mmap (fun _ => do x ← mkFresh; pure { Param . x := x, ty := IRType.object, borrow := false });
-   (newVDecls, xs) ← qs.size.mfold
+   qs ← ps.mapM (fun _ => do x ← mkFresh; pure { Param . x := x, ty := IRType.object, borrow := false });
+   (newVDecls, xs) ← qs.size.foldM
      (fun i (r : Array FnBody × Array Arg) =>
         let (newVDecls, xs) := r;
         let p := ps.get! i;
@@ -225,7 +225,7 @@ match x with
 | _         => k x
 
 @[specialize] def castArgsIfNeededAux (xs : Array Arg) (typeFromIdx : Nat → IRType) : M (Array Arg × Array FnBody) :=
-xs.miterate (#[], #[]) $ fun i (x : Arg) (r : Array Arg × Array FnBody) =>
+xs.iterateM (#[], #[]) $ fun i (x : Arg) (r : Array Arg × Array FnBody) =>
   let expected := typeFromIdx i.val;
   let (xs, bs) := r;
   match x with
@@ -307,7 +307,7 @@ partial def visitFnBody : FnBody → M FnBody
   FnBody.mdata d <$> visitFnBody b
 | FnBody.case tid x _ alts   => do
   let expected := getScrutineeType alts;
-  alts ← alts.mmap $ fun alt => alt.mmodifyBody visitFnBody;
+  alts ← alts.mapM $ fun alt => alt.mmodifyBody visitFnBody;
   castVarIfNeeded x expected $ fun x => do
     pure $ FnBody.case tid x expected alts
 | FnBody.ret x             => do
diff --git a/library/Init/Lean/Compiler/IR/Checker.lean b/library/Init/Lean/Compiler/IR/Checker.lean
index 8109ca42f8..3debe8b48b 100644
--- a/library/Init/Lean/Compiler/IR/Checker.lean
+++ b/library/Init/Lean/Compiler/IR/Checker.lean
@@ -50,7 +50,7 @@ match a with
 | other     => pure ()
 
 def checkArgs (as : Array Arg) : M Unit :=
-as.mfor checkArg
+as.forM checkArg
 
 @[inline] def checkEqTypes (ty₁ ty₂ : IRType) : M Unit :=
 unless (ty₁ == ty₂) $ throw ("unexpected type")
@@ -112,7 +112,7 @@ def checkExpr (ty : IRType) : Expr → M Unit
 
 @[inline] def withParams (ps : Array Param) (k : M Unit) : M Unit :=
 do ctx ← read;
-   localCtx ← ps.mfoldl (fun (ctx : LocalContext) p => do
+   localCtx ← ps.foldlM (fun (ctx : LocalContext) p => do
       markVar p.x;
       pure $ ctx.addParam p) ctx.localCtx;
    adaptReader (fun _ => { localCtx := localCtx, .. ctx }) k
@@ -138,7 +138,7 @@ partial def checkFnBody : FnBody → M Unit
 | FnBody.mdata _ b        => checkFnBody b
 | FnBody.jmp j ys         => checkJP j *> checkArgs ys
 | FnBody.ret x            => checkArg x
-| FnBody.case _ x _ alts  => checkVar x *> alts.mfor (fun alt => checkFnBody alt.body)
+| FnBody.case _ x _ alts  => checkVar x *> alts.forM (fun alt => checkFnBody alt.body)
 | FnBody.unreachable      => pure ()
 
 def checkDecl : Decl → M Unit
@@ -154,7 +154,7 @@ do env ← getEnv;
    | other            => pure ()
 
 def checkDecls (decls : Array Decl) : CompilerM Unit :=
-decls.mfor (checkDecl decls)
+decls.forM (checkDecl decls)
 
 end IR
 end Lean
diff --git a/library/Init/Lean/Compiler/IR/CompilerM.lean b/library/Init/Lean/Compiler/IR/CompilerM.lean
index 2144ec1e82..6008ae2e1c 100644
--- a/library/Init/Lean/Compiler/IR/CompilerM.lean
+++ b/library/Init/Lean/Compiler/IR/CompilerM.lean
@@ -121,7 +121,7 @@ def addDecl (decl : Decl) : CompilerM Unit :=
 modifyEnv (fun env => declMapExt.addEntry env decl)
 
 def addDecls (decls : Array Decl) : CompilerM Unit :=
-decls.mfor addDecl
+decls.forM addDecl
 
 def findEnvDecl' (env : Environment) (n : Name) (decls : Array Decl) : Option Decl :=
 match decls.find? (fun decl => if decl.name == n then some decl else none) with
diff --git a/library/Init/Lean/Compiler/IR/Default.lean b/library/Init/Lean/Compiler/IR/Default.lean
index bd31ca5a68..a6663fd26a 100644
--- a/library/Init/Lean/Compiler/IR/Default.lean
+++ b/library/Init/Lean/Compiler/IR/Default.lean
@@ -66,7 +66,7 @@ do env ← getEnv;
      let decl := ExplicitBoxing.mkBoxedVersion decl;
      let decls : Array Decl := #[decl];
      decls ← explicitRC decls;
-     decls.mfor $ fun decl => modifyEnv $ fun env => addDeclAux env decl;
+     decls.forM $ fun decl => modifyEnv $ fun env => addDeclAux env decl;
      pure ()
 
 -- Remark: we are ignoring the `Log` here. This should be fine.
diff --git a/library/Init/Lean/Compiler/IR/ElimDeadBranches.lean b/library/Init/Lean/Compiler/IR/ElimDeadBranches.lean
index f56c53844f..db66a5d6b2 100644
--- a/library/Init/Lean/Compiler/IR/ElimDeadBranches.lean
+++ b/library/Init/Lean/Compiler/IR/ElimDeadBranches.lean
@@ -151,7 +151,7 @@ partial def projValue : Value → Nat → Value
 | v, _         => v
 
 def interpExpr : Expr → M Value
-| Expr.ctor i ys => ctor i <$> ys.mmap (fun y => findArgValue y)
+| Expr.ctor i ys => ctor i <$> ys.mapM (fun y => findArgValue y)
 | Expr.proj i x  => do v ← findVarValue x; pure $ projValue v i
 | Expr.fap fid ys => do
   ctx ← read;
@@ -179,7 +179,7 @@ do ctx ← read;
 def updateJPParamsAssignment (ys : Array Param) (xs : Array Arg) : M Bool :=
 do ctx ← read;
    let currFnIdx := ctx.currFnIdx;
-   ys.size.mfold (fun i r => do
+   ys.size.foldM (fun i r => do
      let y := ys.get! i;
      let x := xs.get! i;
      yVal ← findVarValue y.x;
@@ -201,7 +201,7 @@ partial def interpFnBody : FnBody → M Unit
     interpFnBody b
 | FnBody.case _ x _ alts => do
   v ← findVarValue x;
-  alts.mfor $ fun alt =>
+  alts.forM $ fun alt =>
     match alt with
     | Alt.ctor i b  => when (containsCtor v i) $ interpFnBody b
     | Alt.default b => interpFnBody b
@@ -220,14 +220,14 @@ partial def interpFnBody : FnBody → M Unit
 def inferStep : M Bool :=
 do ctx ← read;
    modify $ fun s => { assignments := ctx.decls.map $ fun _ => {}, .. s };
-   ctx.decls.size.mfold (fun idx modified => do
+   ctx.decls.size.foldM (fun idx modified => do
      match ctx.decls.get! idx with
      | Decl.fdecl fid ys _ b => do
        s ← get;
        -- dbgTrace (">> " ++ toString fid) $ fun _ =>
        let currVals := s.funVals.get! idx;
        adaptReader (fun (ctx : InterpContext) => { currFnIdx := idx, .. ctx }) $ do
-         ys.mfor $ fun y => updateVarAssignment y.x top;
+         ys.forM $ fun y => updateVarAssignment y.x top;
          interpFnBody b;
        s ← get;
        let newVals := s.funVals.get! idx;
diff --git a/library/Init/Lean/Compiler/IR/EmitC.lean b/library/Init/Lean/Compiler/IR/EmitC.lean
index 9241d3cee8..e697a3ae61 100644
--- a/library/Init/Lean/Compiler/IR/EmitC.lean
+++ b/library/Init/Lean/Compiler/IR/EmitC.lean
@@ -46,7 +46,7 @@ modify (fun out => out ++ toString a)
 emit a *> emit "\n"
 
 def emitLns {α : Type} [HasToString α] (as : List α) : M Unit :=
-as.mfor $ fun a => emitLn a
+as.forM $ fun a => emitLn a
 
 def argToCString (x : Arg) : String :=
 match x with
@@ -106,7 +106,7 @@ do let ps := decl.params;
      if ps.size > closureMaxArgs && isBoxedName decl.name then
        emit "lean_object**"
      else
-       ps.size.mfor $ fun i => do {
+       ps.size.forM $ fun i => do {
          when (i > 0) (emit ", ");
          emit (toCType (ps.get! i).ty)
        };
@@ -130,7 +130,7 @@ do env ← getEnv;
    let modDecls  : NameSet := decls.foldl (fun s d => s.insert d.name) {};
    let usedDecls : NameSet := decls.foldl (fun s d => collectUsedDecls env d (s.insert d.name)) {};
    let usedDecls := usedDecls.toList;
-   usedDecls.mfor $ fun n => do
+   usedDecls.forM $ fun n => do
      decl ← getDecl n;
      match getExternNameFor env `c decl.name with
      | some cName => emitExternDeclAux decl cName
@@ -190,7 +190,7 @@ do env ← getEnv;
    pure $ decls.any (fun d => d.name == `main)
 
 def emitMainFnIfNeeded : M Unit :=
-mwhen hasMainFn emitMainFn
+whenM hasMainFn emitMainFn
 
 def emitFileHeader : M Unit :=
 do env ← getEnv;
@@ -198,7 +198,7 @@ do env ← getEnv;
    emitLn "// Lean compiler output";
    emitLn ("// Module: " ++ toString modName);
    emit "// Imports:";
-   env.imports.mfor $ fun m => emit (" " ++ toString m);
+   env.imports.forM $ fun m => emit (" " ++ toString m);
    emitLn "";
    emitLn "#include \"runtime/lean.h\"";
    emitLns [
@@ -235,7 +235,7 @@ def declareVar (x : VarId) (t : IRType) : M Unit :=
 do emit (toCType t); emit " "; emit x; emit "; "
 
 def declareParams (ps : Array Param) : M Unit :=
-ps.mfor $ fun p => declareVar p.x p.ty
+ps.forM $ fun p => declareVar p.x p.ty
 
 partial def declareVars : FnBody → Bool → M Bool
 | e@(FnBody.vdecl x t _ b), d => do
@@ -271,7 +271,7 @@ match isIf alts with
 | _ => do
   emit "switch ("; emitTag x xType; emitLn ") {";
   let alts := ensureHasDefault alts;
-  alts.mfor $ fun alt => match alt with
+  alts.forM $ fun alt => match alt with
     | Alt.ctor c b  => emit "case " *> emit c.cidx *> emitLn ":" *> emitBody b
     | Alt.default b => emitLn "default: " *> emitBody b;
   emitLn "}"
@@ -322,7 +322,7 @@ do match t with
 def emitJmp (j : JoinPointId) (xs : Array Arg) : M Unit :=
 do ps ← getJPParams j;
    unless (xs.size == ps.size) (throw "invalid goto");
-    xs.size.mfor $ fun i => do {
+    xs.size.forM $ fun i => do {
       let p := ps.get! i;
       let x := xs.get! i;
       emit p.x; emit " = "; emitArg x; emitLn ";"
@@ -333,7 +333,7 @@ def emitLhs (z : VarId) : M Unit :=
 do emit z; emit " = "
 
 def emitArgs (ys : Array Arg) : M Unit :=
-ys.size.mfor $ fun i => do
+ys.size.forM $ fun i => do
   when (i > 0) (emit ", ");
   emitArg (ys.get! i)
 
@@ -347,7 +347,7 @@ do emit "lean_alloc_ctor("; emit c.cidx; emit ", "; emit c.size; emit ", ";
    emitCtorScalarSize c.usize c.ssize; emitLn ");"
 
 def emitCtorSetArgs (z : VarId) (ys : Array Arg) : M Unit :=
-ys.size.mfor $ fun i => do
+ys.size.forM $ fun i => do
   emit "lean_ctor_set("; emit z; emit ", "; emit i; emit ", "; emitArg (ys.get! i); emitLn ");"
 
 def emitCtor (z : VarId) (c : CtorInfo) (ys : Array Arg) : M Unit :=
@@ -359,7 +359,7 @@ do emitLhs z;
 
 def emitReset (z : VarId) (n : Nat) (x : VarId) : M Unit :=
 do emit "if (lean_is_exclusive("; emit x; emitLn ")) {";
-   n.mfor $ fun i => do {
+   n.forM $ fun i => do {
      emit " lean_ctor_release("; emit x; emit ", "; emit i; emitLn ");"
    };
    emit " "; emitLhs z; emit x; emitLn ";";
@@ -400,7 +400,7 @@ ys.toList.map argToCString
 def emitSimpleExternalCall (f : String) (ps : Array Param) (ys : Array Arg) : M Unit :=
 do emit f; emit "(";
    -- We must remove irrelevant arguments to extern calls.
-   ys.size.mfold
+   ys.size.foldM
      (fun i (first : Bool) =>
        if (ps.get! i).ty.isIrrelevant then
          pure first
@@ -430,7 +430,7 @@ def emitPartialApp (z : VarId) (f : FunId) (ys : Array Arg) : M Unit :=
 do decl ← getDecl f;
    let arity := decl.params.size;
    emitLhs z; emit "lean_alloc_closure((void*)("; emitCName f; emit "), "; emit arity; emit ", "; emit ys.size; emitLn ");";
-   ys.size.mfor $ fun i => do {
+   ys.size.forM $ fun i => do {
      let y := ys.get! i;
      emit "lean_closure_set("; emit z; emit ", "; emit i; emit ", "; emitArg y; emitLn ");"
    }
@@ -559,21 +559,21 @@ match v with
   unless (ps.size == ys.size) (throw "invalid tail call");
   if overwriteParam ps ys then do {
     emitLn "{";
-    ps.size.mfor $ fun i => do {
+    ps.size.forM $ fun i => do {
       let p := ps.get! i;
       let y := ys.get! i;
       unless (paramEqArg p y) $ do {
         emit (toCType p.ty); emit " _tmp_"; emit i; emit " = "; emitArg y; emitLn ";"
       }
     };
-    ps.size.mfor $ fun i => do {
+    ps.size.forM $ fun i => do {
       let p := ps.get! i;
       let y := ys.get! i;
       unless (paramEqArg p y) (do emit p.x; emit " = _tmp_"; emit i; emitLn ";")
     };
     emitLn "}"
   } else do {
-    ys.size.mfor $ fun i => do {
+    ys.size.forM $ fun i => do {
       let p := ps.get! i;
       let y := ys.get! i;
       unless (paramEqArg p y) (do emit p.x; emit " = "; emitArg y; emitLn ";")
@@ -627,7 +627,7 @@ do env ← getEnv;
          if xs.size > closureMaxArgs && isBoxedName d.name then
            emit "lean_object** _args"
          else
-           xs.size.mfor $ fun i => do {
+           xs.size.forM $ fun i => do {
              when (i > 0) (emit ", ");
              let x := xs.get! i;
              emit (toCType x.ty); emit " "; emit x.x
@@ -638,7 +638,7 @@ do env ← getEnv;
        };
        emitLn " {";
        when (xs.size > closureMaxArgs && isBoxedName d.name) $
-         xs.size.mfor $ fun i => do {
+         xs.size.forM $ fun i => do {
            let x := xs.get! i;
            emit "lean_object* "; emit x.x; emit " = _args["; emit i; emitLn "];"
          };
@@ -656,7 +656,7 @@ catch
 def emitFns : M Unit :=
 do env ← getEnv;
    let decls := getDecls env;
-   decls.reverse.mfor emitDecl
+   decls.reverse.forM emitDecl
 
 def emitMarkPersistent (d : Decl) (n : Name) : M Unit :=
 when d.resultType.isObj $ do {
@@ -684,7 +684,7 @@ do env ← getEnv;
 def emitInitFn : M Unit :=
 do env ← getEnv;
    modName ← getModName;
-   env.imports.mfor $ fun m => emitLn ("lean_object* initialize_" ++ m.mangle "" ++ "(lean_object*);");
+   env.imports.forM $ fun m => emitLn ("lean_object* initialize_" ++ m.mangle "" ++ "(lean_object*);");
    emitLns [
      "static bool _G_initialized = false;",
      "lean_object* initialize_" ++ modName.mangle "" ++ "(lean_object* w) {",
@@ -692,12 +692,12 @@ do env ← getEnv;
      "if (_G_initialized) return lean_mk_io_result(lean_box(0));",
      "_G_initialized = true;"
    ];
-   env.imports.mfor $ fun m => emitLns [
+   env.imports.forM $ fun m => emitLns [
      "res = initialize_" ++ m.mangle "" ++ "(lean_io_mk_world());",
      "if (lean_io_result_is_error(res)) return res;",
      "lean_dec_ref(res);"];
    let decls := getDecls env;
-   decls.reverse.mfor emitDeclInit;
+   decls.reverse.forM emitDeclInit;
    emitLns ["return lean_mk_io_result(lean_box(0));", "}"]
 
 def main : M Unit :=
diff --git a/library/Init/Lean/Compiler/IR/EmitUtil.lean b/library/Init/Lean/Compiler/IR/EmitUtil.lean
index cd52c02c76..7dd2da4725 100644
--- a/library/Init/Lean/Compiler/IR/EmitUtil.lean
+++ b/library/Init/Lean/Compiler/IR/EmitUtil.lean
@@ -69,7 +69,7 @@ partial def collectFnBody : FnBody → M Unit
   | Expr.pap f _ => collect f *> collectFnBody b
   | other        => collectFnBody b
 | FnBody.jdecl _ _ v b   => collectFnBody v *> collectFnBody b
-| FnBody.case _ _ _ alts => alts.mfor $ fun alt => collectFnBody alt.body
+| FnBody.case _ _ _ alts => alts.forM $ fun alt => collectFnBody alt.body
 | e => unless e.isTerminal $ collectFnBody e.body
 
 def collectInitDecl (fn : Name) : M Unit :=
diff --git a/library/Init/Lean/Compiler/IR/ExpandResetReuse.lean b/library/Init/Lean/Compiler/IR/ExpandResetReuse.lean
index c456c9270e..ab1d45a4c4 100644
--- a/library/Init/Lean/Compiler/IR/ExpandResetReuse.lean
+++ b/library/Init/Lean/Compiler/IR/ExpandResetReuse.lean
@@ -140,7 +140,7 @@ def mkFresh : M VarId :=
 modifyGet $ fun n => ({ idx := n }, n + 1)
 
 def releaseUnreadFields (y : VarId) (mask : Mask) (b : FnBody) : M FnBody :=
-mask.size.mfold
+mask.size.foldM
   (fun i b =>
     match mask.get! i with
     | some _ => pure b -- code took ownership of this field
@@ -268,7 +268,7 @@ partial def searchAndExpand : FnBody → Array FnBody → M FnBody
   v ← searchAndExpand v #[];
   searchAndExpand b (push bs (FnBody.jdecl j xs v FnBody.nil))
 | FnBody.case tid x xType alts,   bs => do
-  alts ← alts.mmap $ fun alt => alt.mmodifyBody $ fun b => searchAndExpand b #[];
+  alts ← alts.mapM $ fun alt => alt.mmodifyBody $ fun b => searchAndExpand b #[];
   pure $ reshape bs (FnBody.case tid x xType alts)
 | b, bs =>
   if b.isTerminal then pure $ reshape bs b
diff --git a/library/Init/Lean/Compiler/IR/NormIds.lean b/library/Init/Lean/Compiler/IR/NormIds.lean
index 1173e2d75f..154e065aa0 100644
--- a/library/Init/Lean/Compiler/IR/NormIds.lean
+++ b/library/Init/Lean/Compiler/IR/NormIds.lean
@@ -90,7 +90,7 @@ fun m => do
 
 @[inline] def withParams {α : Type} (ps : Array Param) (k : Array Param → N α) : N α :=
 fun m => do
-  m ← ps.mfoldl (fun (m : IndexRenaming) p => do n ← getModify (fun n => n + 1); pure $ m.insert p.x.idx n) m;
+  m ← ps.foldlM (fun (m : IndexRenaming) p => do n ← getModify (fun n => n + 1); pure $ m.insert p.x.idx n) m;
   let ps := ps.map $ fun p => { x := normVar p.x m, .. p };
   k ps m
 
@@ -112,7 +112,7 @@ partial def normFnBody : FnBody → N FnBody
 | FnBody.mdata d b        => FnBody.mdata d <$> normFnBody b
 | FnBody.case tid x xType alts => do
   x ← normVar x;
-  alts ← alts.mmap $ fun alt => alt.mmodifyBody normFnBody;
+  alts ← alts.mapM $ fun alt => alt.mmodifyBody normFnBody;
   pure $ FnBody.case tid x xType alts
 | FnBody.jmp j ys        => FnBody.jmp <$> normJP j <*> normArgs ys
 | FnBody.ret x           => FnBody.ret <$> normArg x
diff --git a/library/Init/Lean/Compiler/IR/ResetReuse.lean b/library/Init/Lean/Compiler/IR/ResetReuse.lean
index e0f8aff7ad..f624ef92db 100644
--- a/library/Init/Lean/Compiler/IR/ResetReuse.lean
+++ b/library/Init/Lean/Compiler/IR/ResetReuse.lean
@@ -93,7 +93,7 @@ private partial def Dmain (x : VarId) (c : CtorInfo) : FnBody → M (FnBody × B
   ctx ← read;
   if e.hasLiveVar ctx x then do
     /- If `x` is live in `e`, we recursively process each branch. -/
-    alts ← alts.mmap $ fun alt => alt.mmodifyBody (fun b => Dmain b >>= Dfinalize x c);
+    alts ← alts.mapM $ fun alt => alt.mmodifyBody (fun b => Dmain b >>= Dfinalize x c);
     pure (FnBody.case tid y yType alts, true)
   else pure (e, false)
 | FnBody.jdecl j ys v b   => do
@@ -130,7 +130,7 @@ Dmain x c b >>= Dfinalize x c
 
 partial def R : FnBody → M FnBody
 | FnBody.case tid x xType alts   => do
-    alts ← alts.mmap $ fun alt => do {
+    alts ← alts.mapM $ fun alt => do {
       alt ← alt.mmodifyBody R;
       match alt with
       | Alt.ctor c b =>
diff --git a/library/Init/Lean/Elaborator/Basic.lean b/library/Init/Lean/Elaborator/Basic.lean
index 04baa5ed08..a3e02577ec 100644
--- a/library/Init/Lean/Elaborator/Basic.lean
+++ b/library/Init/Lean/Elaborator/Basic.lean
@@ -350,10 +350,10 @@ def processHeaderAux (baseDir : Option String) (header : Syntax) (trustLevel : U
 do let header     := header.asNode;
    let imports    := if (header.getArg 0).isNone then [`init.default] else [];
    let modImports := (header.getArg 1).getArgs;
-   imports ← modImports.mfoldl (fun imports stx =>
+   imports ← modImports.foldlM (fun imports stx =>
      -- `stx` is of the form `(Module.import "import" (null ...))
      let importPaths := (stx.getArg 1).getArgs; -- .asNode.getArgs;
-     importPaths.mfoldl (fun imports stx => do
+     importPaths.foldlM (fun imports stx => do
        -- `stx` is of the form `(Module.importPath (null "*"*) <id>)
        let stx := stx.asNode;
        let rel := stx.getArg 0;
diff --git a/library/Init/Lean/Elaborator/Command.lean b/library/Init/Lean/Elaborator/Command.lean
index 73e901398a..d55139ecae 100644
--- a/library/Init/Lean/Elaborator/Command.lean
+++ b/library/Init/Lean/Elaborator/Command.lean
@@ -76,7 +76,7 @@ fun n => do
   when (ns == currNs) $ throw "invalid 'export', self export";
   env ← getEnv;
   let ids := (n.getArg 3).getArgs;
-  aliases ← ids.mfoldl (fun (aliases : List (Name × Name)) (idStx : Syntax) => do {
+  aliases ← ids.foldlM (fun (aliases : List (Name × Name)) (idStx : Syntax) => do {
     let id := idStx.getId;
     let declName := ns ++ id;
     if env.contains declName then
diff --git a/library/Init/Lean/Elaborator/PreTerm.lean b/library/Init/Lean/Elaborator/PreTerm.lean
index d7069022f0..18a6119743 100644
--- a/library/Init/Lean/Elaborator/PreTerm.lean
+++ b/library/Init/Lean/Elaborator/PreTerm.lean
@@ -76,11 +76,11 @@ partial def toLevel : Syntax Expr → Elab Level
   | `Lean.Parser.Level.max    => do
      let args := (stx.getArg 1).getArgs;
      first ← toLevel (args.get! 0);
-     args.mfoldlFrom (fun r arg => Level.max r <$> toLevel arg) first 1
+     args.foldlFromM (fun r arg => Level.max r <$> toLevel arg) first 1
   | `Lean.Parser.Level.imax   => do
      let args := (stx.getArg 1).getArgs;
      first ← toLevel (args.get! 0);
-     args.mfoldlFrom (fun r arg => Level.imax r <$> toLevel arg) first 1
+     args.foldlFromM (fun r arg => Level.imax r <$> toLevel arg) first 1
   | `Lean.Parser.Level.hole   => pure $ Level.mvar Name.anonymous
   | `Lean.Parser.Level.num    => pure $ Level.ofNat $ (stx.getArg 0).toNat
   | `Lean.Parser.Level.ident  => do
@@ -145,7 +145,7 @@ private def processBinder (b : Syntax Expr) : Elab (Array PreTerm) :=
 match b.getKind with
 | `Lean.Parser.Term.simpleBinder   => do
    let args := (b.getArg 0).getArgs;
-   args.mmap $ fun arg => do
+   args.mapM $ fun arg => do
      let id := arg.getId;
      hole ← mkHoleFor arg;
      -- decl ← mkLocalDecl id hole;  -- HACK: this file will be deleted
@@ -155,7 +155,7 @@ match b.getKind with
    let ids     := (b.getArg 1).getArgs;
    let optType := b.getArg 2;
    let optDef  := b.getArg 3;
-   ids.mmap $ fun idStx => do
+   ids.mapM $ fun idStx => do
      let id := idStx.getId;
      type ← if optType.getNumArgs == 0 then mkHoleFor idStx else toPreTerm (optType.getArg 1);
      type ← if optDef.getNumArgs == 0 then pure type else
@@ -174,7 +174,7 @@ match b.getKind with
 | _ => throw "unknown binder kind"
 
 private def processBinders (bs : Array (Syntax Expr)) : Elab (Array PreTerm) :=
-bs.mfoldl (fun r s => do xs ← processBinder s; pure (r ++ xs)) #[]
+bs.foldlM (fun r s => do xs ← processBinder s; pure (r ++ xs)) #[]
 
 @[builtinPreTermElab «forall»] def convertForall : PreTermElab :=
 fun n => do
diff --git a/library/Init/Lean/Elaborator/Term.lean b/library/Init/Lean/Elaborator/Term.lean
index 50bff27d27..305dddac03 100644
--- a/library/Init/Lean/Elaborator/Term.lean
+++ b/library/Init/Lean/Elaborator/Term.lean
@@ -26,7 +26,7 @@ partial def elabTermAux : Syntax Expr → Option Expr → Bool → Elab (Syntax
     | none      => do
       -- recursively expand syntax
       let k := n.getKind;
-      args ← n.getArgs.mmap $ fun arg => elabTermAux arg none true;
+      args ← n.getArgs.mapM $ fun arg => elabTermAux arg none true;
       let newStx := Syntax.node k args;
       -- if it was already expanding just return new node, otherwise invoke old elaborator
       if expanding then
diff --git a/library/Init/Lean/Environment.lean b/library/Init/Lean/Environment.lean
index c61d3cc4a2..29b2d21df5 100644
--- a/library/Init/Lean/Environment.lean
+++ b/library/Init/Lean/Environment.lean
@@ -182,7 +182,7 @@ do initializing ← IO.initializing;
 constant registerEnvExtension {σ : Type} [Inhabited σ] (mkInitial : IO σ) : IO (EnvExtension σ) := default _
 
 private def mkInitialExtensionStates : IO (Array EnvExtensionState) :=
-do exts ← envExtensionsRef.get; exts.mmap $ fun ext => ext.mkInitial
+do exts ← envExtensionsRef.get; exts.mapM $ fun ext => ext.mkInitial
 
 @[export lean_mk_empty_environment]
 def mkEmptyEnvironment (trustLevel : UInt32 := 0) : IO Environment :=
@@ -452,7 +452,7 @@ do pExtDescrs ← persistentEnvExtensionsRef.get;
 
 private def finalizePersistentExtensions (env : Environment) : IO Environment :=
 do pExtDescrs ← persistentEnvExtensionsRef.get;
-   pExtDescrs.miterate env $ fun _ extDescr env => do
+   pExtDescrs.iterateM env $ fun _ extDescr env => do
      let s := extDescr.toEnvExtension.getState env;
      newState ← extDescr.addImportedFn s.importedEntries;
      pure $ extDescr.toEnvExtension.setState env { state := newState, .. s }
@@ -463,8 +463,8 @@ do (_, mods) ← importModulesAux modNames ({}, #[]);
    let const2ModIdx := mods.iterate {} $ fun (modIdx) (mod : ModuleData) (m : HashMap Name ModuleIdx) =>
      mod.constants.iterate m $ fun _ cinfo m =>
        m.insert cinfo.name modIdx.val;
-   constants ← mods.miterate SMap.empty $ fun _ (mod : ModuleData) (cs : ConstMap) =>
-     mod.constants.miterate cs $ fun _ cinfo cs => do {
+   constants ← mods.iterateM SMap.empty $ fun _ (mod : ModuleData) (cs : ConstMap) =>
+     mod.constants.iterateM cs $ fun _ cinfo cs => do {
        when (cs.contains cinfo.name) $ throw (IO.userError ("import failed, environment already contains '" ++ toString cinfo.name ++ "'"));
        pure $ cs.insert cinfo.name cinfo
      };
@@ -482,7 +482,7 @@ do (_, mods) ← importModulesAux modNames ({}, #[]);
    };
    env ← setImportedEntries env mods;
    env ← finalizePersistentExtensions env;
-   env ← mods.miterate env $ fun _ mod env => performModifications env mod.serialized;
+   env ← mods.iterateM env $ fun _ mod env => performModifications env mod.serialized;
    pure env
 
 def regNamespacesExtension : IO (SimplePersistentEnvExtension Name NameSet) :=
@@ -532,7 +532,7 @@ do pExtDescrs ← persistentEnvExtensionsRef.get;
    IO.println ("number of buckets for imported consts: " ++ toString env.constants.numBuckets);
    IO.println ("trust level:                           " ++ toString env.header.trustLevel);
    IO.println ("number of extensions:                  " ++ toString env.extensions.size);
-   pExtDescrs.mfor $ fun extDescr => do {
+   pExtDescrs.forM $ fun extDescr => do {
      IO.println ("extension '" ++ toString extDescr.name ++ "'");
      let s := extDescr.toEnvExtension.getState env;
      let fmt := extDescr.statsFn s.state;
diff --git a/library/Init/Lean/LocalContext.lean b/library/Init/Lean/LocalContext.lean
index 6d12b44762..1403985368 100644
--- a/library/Init/Lean/LocalContext.lean
+++ b/library/Init/Lean/LocalContext.lean
@@ -173,29 +173,29 @@ universes u v
 variables {m : Type u → Type v} [Monad m]
 variable {β : Type u}
 
-@[specialize] def mfoldl (lctx : LocalContext) (f : β → LocalDecl → m β) (b : β) : m β :=
-lctx.decls.mfoldl (fun b decl => match decl with
+@[specialize] def foldlM (lctx : LocalContext) (f : β → LocalDecl → m β) (b : β) : m β :=
+lctx.decls.foldlM (fun b decl => match decl with
   | none      => pure b
   | some decl => f b decl)
   b
 
-@[specialize] def mfor (lctx : LocalContext) (f : LocalDecl → m β) : m PUnit :=
-lctx.decls.mfor $ fun decl => match decl with
+@[specialize] def forM (lctx : LocalContext) (f : LocalDecl → m β) : m PUnit :=
+lctx.decls.forM $ fun decl => match decl with
   | none      => pure PUnit.unit
   | some decl => f decl *> pure PUnit.unit
 
-@[specialize] def mfindDecl (lctx : LocalContext) (f : LocalDecl → m (Option β)) : m (Option β) :=
-lctx.decls.mfind $ fun decl => match decl with
+@[specialize] def findDeclM (lctx : LocalContext) (f : LocalDecl → m (Option β)) : m (Option β) :=
+lctx.decls.findM $ fun decl => match decl with
   | none      => pure none
   | some decl => f decl
 
-@[specialize] def mfindDeclRev (lctx : LocalContext) (f : LocalDecl → m (Option β)) : m (Option β) :=
-lctx.decls.mfindRev $ fun decl => match decl with
+@[specialize] def findDeclRevM (lctx : LocalContext) (f : LocalDecl → m (Option β)) : m (Option β) :=
+lctx.decls.findRevM $ fun decl => match decl with
   | none      => pure none
   | some decl => f decl
 
-@[specialize] def mfoldlFrom (lctx : LocalContext) (f : β → LocalDecl → m β) (b : β) (decl : LocalDecl) : m β :=
-lctx.decls.mfoldlFrom (fun b decl => match decl with
+@[specialize] def foldlFromM (lctx : LocalContext) (f : β → LocalDecl → m β) (b : β) (decl : LocalDecl) : m β :=
+lctx.decls.foldlFromM (fun b decl => match decl with
   | none      => pure b
   | some decl => f b decl)
   b decl.index
@@ -203,16 +203,16 @@ lctx.decls.mfoldlFrom (fun b decl => match decl with
 end
 
 @[inline] def foldl {β} (lctx : LocalContext) (f : β → LocalDecl → β) (b : β) : β :=
-Id.run $ lctx.mfoldl f b
+Id.run $ lctx.foldlM f b
 
 @[inline] def findDecl {β} (lctx : LocalContext) (f : LocalDecl → Option β) : Option β :=
-Id.run $ lctx.mfindDecl f
+Id.run $ lctx.findDeclM f
 
 @[inline] def findDeclRev {β} (lctx : LocalContext) (f : LocalDecl → Option β) : Option β :=
-Id.run $ lctx.mfindDeclRev f
+Id.run $ lctx.findDeclRevM f
 
 @[inline] def foldlFrom {β} (lctx : LocalContext) (f : β → LocalDecl → β) (b : β) (decl : LocalDecl) : β :=
-Id.run $ lctx.mfoldlFrom f b decl
+Id.run $ lctx.foldlFromM f b decl
 
 partial def isSubPrefixOfAux (a₁ a₂ : PArray (Option LocalDecl)) : Nat → Nat → Bool
 | i, j =>
diff --git a/library/Init/Lean/Parser/Module.lean b/library/Init/Lean/Parser/Module.lean
index ceddb445d9..18a43abb93 100644
--- a/library/Init/Lean/Parser/Module.lean
+++ b/library/Init/Lean/Parser/Module.lean
@@ -91,7 +91,7 @@ private partial def testModuleParserAux (env : Environment) (c : ParserContextCo
   match parseCommand env c s messages with
   | (stx, s, messages) =>
     if isEOI stx || isExitCommand stx then do
-      messages.toList.mfor $ fun msg => IO.println msg;
+      messages.toList.forM $ fun msg => IO.println msg;
       pure (!messages.hasErrors)
     else do
       when displayStx (IO.println stx);
@@ -114,7 +114,7 @@ partial def parseFileAux (env : Environment) (ctx : ParserContextCore) : ModuleP
         let stx := mkListNode stxs;
         pure stx.updateLeading
       else do
-        msgs.toList.mfor $ fun msg => IO.println msg;
+        msgs.toList.forM $ fun msg => IO.println msg;
         throw (IO.userError "failed to parse file")
     else
       parseFileAux state msgs (stxs.push stx)
diff --git a/library/Init/Lean/Path.lean b/library/Init/Lean/Path.lean
index 7f95a60e13..f76160c72d 100644
--- a/library/Init/Lean/Path.lean
+++ b/library/Init/Lean/Path.lean
@@ -26,7 +26,7 @@ do curr ← realPathNormalized ".";
 constant searchPathRef : IO.Ref (Array String) := default _
 
 def setSearchPath (s : List String) : IO Unit :=
-do s ← s.mmap realPathNormalized;
+do s ← s.mapM realPathNormalized;
    searchPathRef.set s.toArray
 
 def getBuiltinSearchPath : IO (List String) :=
@@ -67,7 +67,7 @@ let checkFile (curr : String) : IO (Option String) := do {
 };
 do let fname := System.FilePath.normalizePath fname;
    paths ← searchPathRef.get;
-   paths.mfind $ fun path => do
+   paths.findM $ fun path => do
      let curr := path ++ pathSep ++ fname;
      result ← checkFile (curr ++ toString extSeparator ++ ext);
      match result with
diff --git a/library/Init/Lean/Syntax.lean b/library/Init/Lean/Syntax.lean
index 79223d4002..e643ff2b54 100644
--- a/library/Init/Lean/Syntax.lean
+++ b/library/Init/Lean/Syntax.lean
@@ -188,12 +188,12 @@ stx.asNode.getKind
   o ← fn stx;
   match o with
   | some stx => pure stx
-  | none     => do args ← args.mmap mreplace; pure (node kind args)
+  | none     => do args ← args.mapM mreplace; pure (node kind args)
 | stx => do o ← fn stx; pure $ o.getD stx
 
 @[specialize] partial def mrewriteBottomUp {α} {m : Type → Type} [Monad m] (fn : Syntax α → m (Syntax α)) : Syntax α → m (Syntax α)
 | node kind args   => do
-  args ← args.mmap mrewriteBottomUp;
+  args ← args.mapM mrewriteBottomUp;
   fn (node kind args)
 | stx => fn stx
 
@@ -298,8 +298,8 @@ partial def reprint {α} : Syntax α → Option String
     if args.size == 0 then failure
     else do
       s ← reprint (args.get! 0);
-      args.mfoldlFrom (fun s stx => do s' ← reprint stx; guard (s == s'); pure s) s 1
-  else args.mfoldl (fun r stx => do s ← reprint stx; pure $ r ++ s) ""
+      args.foldlFromM (fun s stx => do s' ← reprint stx; guard (s == s'); pure s) s 1
+  else args.foldlM (fun r stx => do s ← reprint stx; pure $ r ++ s) ""
 | _ => ""
 
 open Lean.Format
diff --git a/library/Init/Lean/Trace.lean b/library/Init/Lean/Trace.lean
index 206fc370cf..fb32a21b07 100644
--- a/library/Init/Lean/Trace.lean
+++ b/library/Init/Lean/Trace.lean
@@ -40,7 +40,7 @@ private def addTrace (cls : Name) (msg : MessageData) : m Unit :=
 modifyTraces $ fun traces => traces.push (MessageData.tagged cls msg)
 
 @[inline] protected def trace (cls : Name) (msg : Unit → MessageData) : m Unit :=
-mwhen (isTracingEnabledFor cls) (addTrace cls (msg ()))
+whenM (isTracingEnabledFor cls) (addTrace cls (msg ()))
 
 @[inline] def traceCtx (cls : Name) (ctx : m α) : m α :=
 do b ← isTracingEnabledFor cls;
diff --git a/library/Init/Lean/TypeClass/Context.lean b/library/Init/Lean/TypeClass/Context.lean
index 87aa3d9783..140c262690 100644
--- a/library/Init/Lean/TypeClass/Context.lean
+++ b/library/Init/Lean/TypeClass/Context.lean
@@ -213,12 +213,12 @@ partial def eUnify : Expr → Expr → EState String Context Unit
     else if e₁.isBVar && e₂.isBVar && e₁.bvarIdx == e₂.bvarIdx then pure ()
     else if e₁.isFVar && e₂.isFVar && e₁.fvarName == e₂.fvarName then pure ()
     else if e₁.isConst && e₂.isConst && e₁.constName == e₂.constName then
-      List.mfor₂ uUnify e₁.constLevels e₂.constLevels
+      List.forM₂ uUnify e₁.constLevels e₂.constLevels
     else if e₁.isApp && e₂.isApp && e₁.getAppNumArgs == e₂.getAppNumArgs then do
       let args₁ := e₁.getAppArgs;
       let args₂ := e₂.getAppArgs;
       eUnify e₁.getAppFn e₂.getAppFn;
-      args₁.size.mfor $ fun i => eUnify (args₁.get! i) (args₂.get! i)
+      args₁.size.forM $ fun i => eUnify (args₁.get! i) (args₂.get! i)
     else if e₁.isForall && e₂.isForall then do
       eUnify e₁.bindingDomain e₂.bindingDomain;
       eUnify e₁.bindingBody e₂.bindingBody
diff --git a/library/Init/Lean/TypeClass/Synth.lean b/library/Init/Lean/TypeClass/Synth.lean
index 80f3f128b2..4ef2753712 100644
--- a/library/Init/Lean/TypeClass/Synth.lean
+++ b/library/Init/Lean/TypeClass/Synth.lean
@@ -171,7 +171,7 @@ do lookupStatus ← get >>= λ ϕ => pure $ ϕ.tableEntries.find anormSubgoal;
      if entry.answers.any (λ answer₁ => answer₁.type == answer.type) then pure() else do
        let newEntry : TableEntry := { answers := entry.answers.push answer .. entry };
        modify $ λ ϕ => { tableEntries := ϕ.tableEntries.insert anormSubgoal newEntry .. ϕ };
-       entry.waiters.mfor (wakeUp answer)
+       entry.waiters.forM (wakeUp answer)
 
 def consume : TCMethod Unit :=
 do cNode ← get >>= λ ϕ => pure ϕ.consumerStack.peek!;