diff --git a/tests/bench/binarytrees.lean b/tests/bench/binarytrees.lean
index 9d6a33852a..10349c67ed 100644
--- a/tests/bench/binarytrees.lean
+++ b/tests/bench/binarytrees.lean
@@ -53,7 +53,7 @@ def main : List String → IO UInt32
-- allocate, walk, and deallocate many bottom-up binary trees
let vs := (depth minN maxN); -- `using` (parList $ evalTuple3 r0 r0 rseq)
- vs.mmap (fun ⟨m,d,i⟩ => out (toString m ++ "\t trees") d i.get);
+ vs.mapM (fun ⟨m,d,i⟩ => out (toString m ++ "\t trees") d i.get);
-- confirm the the long-lived binary tree still exists
out "long lived tree" maxN (check long);
diff --git a/tests/bench/qsort.lean b/tests/bench/qsort.lean
index 57c88e3397..d5c85b119b 100644
--- a/tests/bench/qsort.lean
+++ b/tests/bench/qsort.lean
@@ -57,8 +57,8 @@ qsortAux lt as 0 (UInt32.ofNat (as.size - 1))
def main (xs : List String) : IO Unit :=
do
let n := xs.head!.toNat;
-n.mfor $ fun _ =>
-n.mfor $ fun i => do
+n.forM $ fun _ =>
+n.forM $ fun i => do
let xs := mkRandomArray i (UInt32.ofNat i) Array.empty;
let xs := qsort xs (fun a b => a < b);
--IO.println xs;
diff --git a/tests/compiler/phashmap.lean b/tests/compiler/phashmap.lean
index 4dc295605e..4815671f27 100644
--- a/tests/compiler/phashmap.lean
+++ b/tests/compiler/phashmap.lean
@@ -29,7 +29,7 @@ def mkMap (n : Nat) : Map :=
n.fold (fun i m => m.insert i (i*10)) PersistentHashMap.empty
def check (n : Nat) (m : Map) : IO Unit :=
-n.mfor $ fun i =>
+n.forM $ fun i =>
match m.find i with
| none => IO.println ("failed to find " ++ toString i)
| some v => unless (v == i*10) (IO.println ("unexpected value " ++ toString i ++ " => " ++ toString v))
@@ -38,7 +38,7 @@ def delOdd (n : Nat) (m : Map) : Map :=
n.fold (fun i m => if i % 2 == 0 then m else m.erase i) m
def check2 (n : Nat) (bot : Nat) (m : Map) : IO Unit :=
-n.mfor $ fun i =>
+n.forM $ fun i =>
if i % 2 == 0 && i >= bot then
match m.find i with
| none => IO.println ("failed to find " ++ toString i)
diff --git a/tests/compiler/rbmap_library.lean b/tests/compiler/rbmap_library.lean
index f8314d883f..7291f6890e 100644
--- a/tests/compiler/rbmap_library.lean
+++ b/tests/compiler/rbmap_library.lean
@@ -55,7 +55,7 @@ do IO.setRandSeed seed;
IO.println ("tst3 size: " ++ toString a.size);
let m := a.iterate m (fun i ⟨k, v⟩ m => if i.val % 2 == 0 then m.erase k else m);
check (sz m == a.size / 2);
- a.miterate () (fun i ⟨k, v⟩ _ => when (i.val % 2 == 1) (check (m.find k == some v)));
+ a.iterateM () (fun i ⟨k, v⟩ _ => when (i.val % 2 == 1) (check (m.find k == some v)));
IO.println ("tst3 after, depth: " ++ toString (depth m) ++ ", size: " ++ toString (sz m));
pure ()
diff --git a/tests/compiler/termparsertest1.lean b/tests/compiler/termparsertest1.lean
index 5815f6b02e..772e6efd52 100644
--- a/tests/compiler/termparsertest1.lean
+++ b/tests/compiler/termparsertest1.lean
@@ -10,7 +10,7 @@ stx ← IO.ofExcept $ runParser env termPTables input "" "expr";
IO.println stx
def test (is : List String) : IO Unit :=
-is.mfor $ fun input => do
+is.forM $ fun input => do
IO.println input;
testParser input
@@ -23,7 +23,7 @@ match runParser env termPTables input "" "expr" with
| Except.error msg => IO.println ("failed as expected, error: " ++ msg)
def testFailures (is : List String) : IO Unit :=
-is.mfor $ fun input => do
+is.forM $ fun input => do
IO.println input;
testParserFailure input
diff --git a/tests/lean/binsearch.lean b/tests/lean/binsearch.lean
index ccdc08ce5d..f15e091f3b 100644
--- a/tests/lean/binsearch.lean
+++ b/tests/lean/binsearch.lean
@@ -7,7 +7,7 @@ do
let as := mkAssocArray n Array.empty;
IO.println as;
let as := as.qsort (fun a b => a.1 < b.1);
-(2*n).mfor $ fun i => do
+(2*n).forM $ fun i => do
let entry := as.binSearch (i, false) (fun a b => a.1 < b.1);
IO.println (">> " ++ toString i ++ " ==> " ++ toString entry)
diff --git a/tests/lean/ctor_layout.lean b/tests/lean/ctor_layout.lean
index 93c3659634..3de301dc9c 100644
--- a/tests/lean/ctor_layout.lean
+++ b/tests/lean/ctor_layout.lean
@@ -6,13 +6,13 @@ def tst : IO Unit :=
do initSearchPath "../../library:.";
env ← importModules [`Init.Lean.Compiler.IR.Basic];
ctorLayout ← IO.ofExcept $ getCtorLayout env `Lean.IR.Expr.reuse;
- ctorLayout.fieldInfo.mfor $ fun finfo => IO.println (format finfo);
+ ctorLayout.fieldInfo.forM $ fun finfo => IO.println (format finfo);
IO.println "---";
ctorLayout ← IO.ofExcept $ getCtorLayout env `Lean.EnvironmentHeader.mk;
- ctorLayout.fieldInfo.mfor $ fun finfo => IO.println (format finfo);
+ ctorLayout.fieldInfo.forM $ fun finfo => IO.println (format finfo);
IO.println "---";
ctorLayout ← IO.ofExcept $ getCtorLayout env `Subtype.mk;
- ctorLayout.fieldInfo.mfor $ fun finfo => IO.println (format finfo);
+ ctorLayout.fieldInfo.forM $ fun finfo => IO.println (format finfo);
pure ()
#eval tst
diff --git a/tests/lean/ref1.lean b/tests/lean/ref1.lean
index 809b3333ae..4ea83e08b2 100644
--- a/tests/lean/ref1.lean
+++ b/tests/lean/ref1.lean
@@ -4,18 +4,18 @@ do v ← r.get;
IO.println (">> " ++ toString v)
def initArray (r : IO.Ref (Array Nat)) (n : Nat) : IO Unit :=
-n.mfor $ fun i => do
+n.forM $ fun i => do
r.modify $ fun a => a.push (2*i)
def showArrayRef (r : IO.Ref (Array Nat)) : IO Unit :=
do a ← r.swap ∅;
- a.size.mfor (fun i => IO.println ("[" ++ toString i ++ "]: " ++ toString (a.get! i)));
+ a.size.forM (fun i => IO.println ("[" ++ toString i ++ "]: " ++ toString (a.get! i)));
r.swap a;
pure ()
def tst (n : Nat) : IO Unit :=
do r₁ ← IO.mkRef 0;
- n.mfor $ λ _ => inc r₁;
+ n.forM $ λ _ => inc r₁;
r₂ ← IO.mkRef (∅ : Array Nat);
initArray r₂ n;
showArrayRef r₂