diff --git a/tests/lean/extract.lean b/tests/lean/extract.lean
index 5a09ef4e4f..30c4de76e9 100644
--- a/tests/lean/extract.lean
+++ b/tests/lean/extract.lean
@@ -1,80 +1,79 @@
-#exit -- Disabled until we implement new VM
 #eval "abc"
 
 /- some "a" -/
 #eval
- let s₁  := "abcde" in
- let it₁ := s₁.mkIterator in
- let it₂ := it₁.next in
+ let s₁  := "abcde";
+ let it₁ := s₁.mkIterator;
+ let it₂ := it₁.next;
  it₁.extract it₂
 
 /- some "" -/
 #eval
- let s₁  := "abcde" in
- let it₁ := s₁.mkIterator in
+ let s₁  := "abcde";
+ let it₁ := s₁.mkIterator;
  it₁.extract it₁
 
 /- none -/
 #eval
- let s₁  := "abcde" in
- let it₁ := s₁.mkIterator in
- let it₂ := it₁.next in
+ let s₁  := "abcde";
+ let it₁ := s₁.mkIterator;
+ let it₂ := it₁.next;
  it₂.extract it₁
 
 /- some "abc" -/
 #eval
- let s₁  := "abcde" in
- let it₁ := s₁.mkIterator in
- let it₂ := it₁.next.next.next.prev.next in
+ let s₁  := "abcde";
+ let it₁ := s₁.mkIterator;
+ let it₂ := it₁.next.next.next.prev.next;
  it₁.extract it₂
 
 /- some "bcde" -/
 #eval
- let s₁  := "abcde" in
- let it₁ := s₁.mkIterator.next in
- let it₂ := it₁.next.next.next.next in
+ let s₁  := "abcde";
+ let it₁ := s₁.mkIterator.next;
+ let it₂ := it₁.next.next.next.next;
  it₁.extract it₂
 
 /- some "abcde" -/
 #eval
- let s₁  := "abcde" in
- let it₁ := s₁.mkIterator in
- let it₂ := it₁.next.next.next.next.next in
+ let s₁  := "abcde";
+ let it₁ := s₁.mkIterator;
+ let it₂ := it₁.next.next.next.next.next;
  it₁.extract it₂
 
 /- some "ab" -/
 #eval
-  let s₁  := "abcde" in
-  let s₂  := "abcde" in
-  let it₁ := s₁.mkIterator in
-  let it₂ := s₂.mkIterator.next.next in
+  let s₁  := "abcde";
+  let s₂  := "abcde";
+  let it₁ := s₁.mkIterator;
+  let it₂ := s₂.mkIterator.next.next;
   it₁.extract it₂
 
 /- none -/
 #eval
-  let s₁  := "abcde" in
-  let s₂  := "abhde" in
-  let it₁ := s₁.mkIterator in
-  let it₂ := s₂.mkIterator.next.next in
+  let s₁  := "abcde";
+  let s₂  := "abhde";
+  let it₁ := s₁.mkIterator;
+  let it₂ := s₂.mkIterator.next.next;
   it₁.extract it₂
 
 /- none -/
 #eval
-  let s₁  := "abcde" in
-  let it₁ := s₁.mkIterator in
-  let it₂ := it₁.next.setCurr 'a' in
+  let s₁  := "abcde";
+  let it₁ := s₁.mkIterator;
+  let it₂ := it₁.next.setCurr 'a';
   it₁.extract it₂
 
 /- some "a" -/
 #eval
-  let s₁  := "abcde" in
-  let it₁ := s₁.mkIterator in
-  let it₂ := it₁.next.setCurr 'b' in
+  let s₁  := "abcde";
+  let it₁ := s₁.mkIterator;
+  let it₂ := it₁.next.setCurr 'b';
   it₁.extract it₂
 
 /- some "a" -/
 #eval
-  let s₁  := "abcde" in
-  let it₁ := s₁.mkIterator in
-  let it₂ := (it₁.next.setCurr 'a').setCurr 'b' in
+  let s₁  := "abcde";
+  let it₁ := s₁.mkIterator;
+  let it₂ := (it₁.next.setCurr 'a').setCurr 'b';
   it₁.extract it₂
diff --git a/tests/lean/extract.lean.expected.out b/tests/lean/extract.lean.expected.out
index 79697375ba..c7329d7f10 100644
--- a/tests/lean/extract.lean.expected.out
+++ b/tests/lean/extract.lean.expected.out
@@ -1 +1,12 @@
-extract.lean:1:0: warning: using 'exit' to interrupt Lean
+"abc"
+"a"
+""
+""
+"abc"
+"bcde"
+"abcde"
+"ab"
+""
+""
+"a"
+"a"
diff --git a/tests/lean/repr_issue.lean b/tests/lean/repr_issue.lean
index 5651e61f14..29d2d32d37 100644
--- a/tests/lean/repr_issue.lean
+++ b/tests/lean/repr_issue.lean
@@ -9,8 +9,6 @@ foo
 def ex₂ : ExceptT String (StateT (Array Nat) Id) Nat :=
 foo
 
-#exit
-
 -- The following examples were producing an element of Type `id (Except String Nat)`.
 -- Type class resolution was failing to produce an instance for `HasRepr (id (Except String Nat))` because `id` is not transparent.
 #eval run ex₁ (mkArray 10 1000)
diff --git a/tests/lean/repr_issue.lean.expected.out b/tests/lean/repr_issue.lean.expected.out
index b267fa18dc..1e7e4f8c81 100644
--- a/tests/lean/repr_issue.lean.expected.out
+++ b/tests/lean/repr_issue.lean.expected.out
@@ -1 +1,2 @@
-repr_issue.lean:12:0: warning: using 'exit' to interrupt Lean
+(ok 1000)
+(ok 33)
diff --git a/tests/lean/run/array1.lean b/tests/lean/run/array1.lean
index 652065af44..41deab4445 100644
--- a/tests/lean/run/array1.lean
+++ b/tests/lean/run/array1.lean
@@ -14,7 +14,7 @@ a.foldl Nat.add 0
 #exit
 
 #eval mkArray 4 1
-#eval Array.map (+10) v
+#eval Array.map (fun x => x+10) v
 #eval f ⟨1, sorry⟩
 #eval f ⟨9, sorry⟩
 #eval (((mkArray 1 1).push 2).push 3).foldl 0 (+)
diff --git a/tests/lean/run/compiler_proj_bug.lean b/tests/lean/run/compiler_proj_bug.lean
index c23b8abb4e..788bd834fb 100644
--- a/tests/lean/run/compiler_proj_bug.lean
+++ b/tests/lean/run/compiler_proj_bug.lean
@@ -4,6 +4,4 @@ structure S :=
 def f (s : S) :=
 s.b - s.a
 
-#exit
-
 #eval f {a := 5, b := 30, h := sorry }
diff --git a/tests/lean/string_imp.lean b/tests/lean/string_imp.lean
index 06e9b4d466..1b69c503d3 100644
--- a/tests/lean/string_imp.lean
+++ b/tests/lean/string_imp.lean
@@ -1,35 +1,12 @@
-#exit -- Disabled until we implement new VM
-
 #eval ("abc" ++ "cde").length
-#eval "abc".popBack
-#eval "".popBack
-#eval "abcd".popBack
 #eval ("abcd".mkIterator.nextn 2).remainingToString
-#eval ("abcd".mkIterator.nextn 2).prevToString
 #eval ("abcd".mkIterator.nextn 10).remainingToString
-#eval ("abcd".mkIterator.nextn 10).prevToString
-#eval "foo.Lean".popnBack 5
-#eval "foo.Lean".backn 5
-#eval "αβγ".popBack
 #eval "αβ".length
-#eval ("αβcc".mkIterator.next.insert "_foo_").toString
-#eval ("αβcc".mkIterator.next.next.insert "_foo_").toString
-#eval ("αβcc".mkIterator.next.next.prev.insert "_foo_").toString
-#eval ("αβcc".mkIterator.remaining)
-#eval ("αβcc".mkIterator.next.remaining)
-#eval ("αβcc".mkIterator.next.insert "αbcβ").remaining
-#eval (("αβcc".mkIterator.next.insert "αbcβ").remove 2).remaining
-#eval (("αβcc".mkIterator.next.insert "αbcβ").remove 2).prev.remaining
-#eval ("αβcc".mkIterator.next.toEnd).remaining
-#eval "αβcc".mkIterator.offset
-#eval "αβcc".mkIterator.next.offset
-#eval "αβcc".mkIterator.next.next.offset
-#eval ("αβcc".mkIterator.next.setCurr 'a').offset
-#eval ("αβcc".mkIterator.next.insert "αbc").offset
-#eval ("αβcc".mkIterator.next.insert "αbc").remaining
-#eval ("αβcc".mkIterator.insert "αbc").offset
-#eval ("αβcc".mkIterator.next.insert "αbcβ").offset
-#eval "αβcd".mkIterator.toEnd.offset
+#eval "αβcc".mkIterator.pos
+#eval "αβcc".mkIterator.next.pos
+#eval "αβcc".mkIterator.next.next.pos
+#eval "αβcc".mkIterator.next.setCurr 'a'
+#eval "αβcd".mkIterator.toEnd.pos
 #eval "ab\n\nfoo bla".lineColumn 0
 #eval "ab\n\nfoo bla".lineColumn 1
 #eval "ab\n\nfoo bla".lineColumn 2
diff --git a/tests/lean/string_imp.lean.expected.out b/tests/lean/string_imp.lean.expected.out
index 22b72a4dd2..bf4bf5bcf2 100644
--- a/tests/lean/string_imp.lean.expected.out
+++ b/tests/lean/string_imp.lean.expected.out
@@ -1 +1,15 @@
-string_imp.lean:1:0: warning: using 'exit' to interrupt Lean
+6
+"cd"
+""
+2
+0
+2
+4
+(String.Iterator.mk "αacc" 2)
+6
+(3, 7)
+(3, 7)
+(3, 7)
+(3, 7)
+(3, 7)
+(3, 7)
diff --git a/tests/lean/string_imp2.lean b/tests/lean/string_imp2.lean
index 424dc14a49..722041021c 100644
--- a/tests/lean/string_imp2.lean
+++ b/tests/lean/string_imp2.lean
@@ -9,20 +9,6 @@ let it₁ := s.mkIterator;
 let it₂ := it₁.next;
 it₁.remainingToString ++ "-" ++ it₂.remainingToString
 
-
-#exit -- Disabled until we implement new VM
-
-def r (s : String) : String :=
-let it₁ := s.mkIterator.toEnd;
-let it₂ := it₁.prev;
-it₁.prevToString ++ "-" ++ it₂.prevToString
-
-def s (s : String) : String :=
-let it₁ := s.mkIterator.toEnd;
-let it₂ := it₁.prev;
-(it₁.insert "abc").toString ++ (it₂.insert "de").toString
-
-
 #eval "hello" ++ "hello"
 #eval f "hello"
 #eval (f "αβ").length
@@ -51,8 +37,6 @@ let it₂ := it₁.prev;
 #eval "abc".mkIterator.remainingToString
 #eval ("a".push (Char.ofNat 0)) ++ "bb"
 #eval (("a".push (Char.ofNat 0)) ++ "αb").length
-#eval r "abc"
-#eval "abc".mkIterator.toEnd.prevToString
 #eval "".mkIterator.hasNext
 #eval "a".mkIterator.hasNext
 #eval "a".mkIterator.next.hasNext
@@ -60,14 +44,5 @@ let it₂ := it₁.prev;
 #eval "a".mkIterator.next.hasPrev
 #eval "αβ".mkIterator.next.hasPrev
 #eval "αβ".mkIterator.next.prev.hasPrev
-#eval ("αβ".mkIterator.toEnd.insert "abc").toString
-#eval ("αβ".mkIterator.next.insert "abc").toString
-#eval s "αβ"
-#eval ("abcdef".mkIterator.next.remove 2).toString
-#eval ("abcdef".mkIterator.next.next.remove 2).toString
-#eval ("abcdef".mkIterator.next.remove 3).toString
-#eval (("abcdef".mkIterator.next.next.next.remove 100).prev.setCurr 'a').toString
-#eval ("abcdef".mkIterator.next.next.next.remove 100).hasNext
-#eval ("abcdef".mkIterator.next.next.next.remove 100).prev.hasNext
-#eval toBool $ "abc" = "abc"
-#eval toBool $ "abc" = "abd"
+#eval "abc" == "abc"
+#eval "abc" == "abd"
diff --git a/tests/lean/string_imp2.lean.expected.out b/tests/lean/string_imp2.lean.expected.out
index 3a5dab16be..0b0ec8edef 100644
--- a/tests/lean/string_imp2.lean.expected.out
+++ b/tests/lean/string_imp2.lean.expected.out
@@ -1 +1,37 @@
-string_imp2.lean:13:0: warning: using 'exit' to interrupt Lean
+"hellohello"
+"hello hello"
+5
+['h', 'e', 'l', 'l', 'o']
+['α', 'β']
+[]
+['α', 'β', 'γ']
+"αβγ"
+"αβγ"
+"αβγ"
+2
+['α', 'β']
+"αβa"
+"α α-"
+'A'
+"aβγ"
+"abγ"
+"abc"
+"cbγ"
+"0bc"
+"01c"
+"012"
+"21c"
+"λbc"
+"abc-bc"
+"abc"
+"a\x00bb"
+4
+false
+true
+false
+false
+true
+true
+false
+true
+false