diff --git a/doc/examples/compiler/test.lean b/doc/examples/compiler/test.lean
index f162825b9e..719dd1a872 100644
--- a/doc/examples/compiler/test.lean
+++ b/doc/examples/compiler/test.lean
@@ -1,3 +1,4 @@
-def main (n : List String) : IO UInt32 :=
-do IO.println (toString n);
+#lang lean4
+def main (n : List String) : IO UInt32 := do
+   IO.println (toString n)
    pure 0
diff --git a/tests/bench/binarytrees.lean b/tests/bench/binarytrees.lean
index ebfa5de7e3..5e5e4e6d40 100644
--- a/tests/bench/binarytrees.lean
+++ b/tests/bench/binarytrees.lean
@@ -1,3 +1,4 @@
+#lang lean4
 inductive Tree
 | Nil
 | Node (l r : Tree) : Tree
@@ -53,7 +54,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.forM (fun ⟨m,d,i⟩ => out (toString m ++ "\t trees") d i.get);
+  vs.forM (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/const_fold.lean b/tests/bench/const_fold.lean
index 801f7cf3e9..33cdb6aad0 100644
--- a/tests/bench/const_fold.lean
+++ b/tests/bench/const_fold.lean
@@ -1,3 +1,4 @@
+#lang lean4
 inductive Expr
 | Var : Nat → Expr
 | Val : Nat → Expr
diff --git a/tests/bench/deriv.lean b/tests/bench/deriv.lean
index 50c00effe5..1c70bc3091 100644
--- a/tests/bench/deriv.lean
+++ b/tests/bench/deriv.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /- Benchmark for new code generator -/
 inductive Expr
 | Val : Int → Expr
@@ -52,10 +53,10 @@ def ln : Expr → Expr
 def d (x : String) : Expr → Expr
 | Val _     => Val 0
 | Var y     => if x = y then Val 1 else Val 0
-| Add f g   => add (d f) (d g)
-| Mul f g   => add (mul f (d g)) (mul g (d f))
-| Pow f g   => mul (pow f g) (add (mul (mul g (d f)) (pow f (Val (-1)))) (mul (ln f) (d g)))
-| Ln f      => mul (d f) (pow f (Val (-1)))
+| Add f g   => add (d x f) (d x g)
+| Mul f g   => add (mul f (d x g)) (mul g (d x f))
+| Pow f g   => mul (pow f g) (add (mul (mul g (d x f)) (pow f (Val (-1)))) (mul (ln f) (d x g)))
+| Ln f      => mul (d x f) (pow f (Val (-1)))
 
 def count : Expr → UInt32
 | Val _   => 1
@@ -65,7 +66,7 @@ def count : Expr → UInt32
 | Pow f g   => count f + count g
 | Ln f      => count f
 
-def Expr.toString : Expr → String
+protected def Expr.toString : Expr → String
 | Val n   => toString n
 | Var x   => x
 | Add f g   => "(" ++ Expr.toString f ++ " + " ++ Expr.toString g ++ ")"
@@ -78,7 +79,7 @@ instance : HasToString Expr :=
 
 def nestAux (s : Nat) (f : Nat → Expr → IO Expr) : Nat → Expr → IO Expr
 | 0,       x => pure x
-| m@(n+1), x => f (s - m) x >>= nestAux n
+| m@(n+1), x => f (s - m) x >>= nestAux s f n
 
 def nest (f : Nat → Expr → IO Expr) (n : Nat) (e : Expr) : IO Expr :=
 nestAux n f n e
diff --git a/tests/bench/qsort.lean b/tests/bench/qsort.lean
index f1c22f0670..ef89c791b4 100644
--- a/tests/bench/qsort.lean
+++ b/tests/bench/qsort.lean
@@ -1,3 +1,4 @@
+#lang lean4
 abbrev Elem := UInt32
 
 def badRand (seed : Elem) : Elem :=
@@ -10,24 +11,25 @@ def mkRandomArray : Nat → Elem → Array Elem → Array Elem
 partial def checkSortedAux (a : Array Elem) : Nat → IO Unit
 | i =>
   if i < a.size - 1 then do
-    unless (a.get! i <= a.get! (i+1)) $ throw (IO.userError "array is not sorted");
-    checkSortedAux (i+1)
+    unless (a.get! i <= a.get! (i+1)) do  throw (IO.userError "array is not sorted");
+    checkSortedAux a (i+1)
   else
     pure ()
 
 -- copied from stdlib, but with `UInt32` indices instead of `Nat` (which is more comparable to the other versions)
 abbrev Idx := UInt32
-instance : HasLift UInt32 Nat := ⟨UInt32.toNat⟩
-prefix `↑`:max := oldCoe
+
+macro:max "↑" x:term:max : term => `(UInt32.toNat $x)
+
 
 @[specialize] private partial def partitionAux {α : Type} [Inhabited α] (lt : α → α → Bool) (hi : Idx) (pivot : α) : Array α → Idx → Idx → Idx × Array α
 | as, i, j =>
   if j < hi then
     if lt (as.get! ↑j) pivot then
       let as := as.swap! ↑i ↑j;
-      partitionAux as (i+1) (j+1)
+      partitionAux lt hi pivot as (i+1) (j+1)
     else
-      partitionAux as i (j+1)
+      partitionAux lt hi pivot as i (j+1)
   else
     let as := as.swap! ↑i ↑hi;
     (i, as)
@@ -47,8 +49,8 @@ partitionAux lt hi pivot as lo lo
     -- TODO: fix `partial` support in the equation compiler, it breaks if we use `let (mid, as) := partition as lt low high`
     let mid := p.1;
     let as  := p.2;
-    let as  := qsortAux as low mid;
-    qsortAux as (mid+1) high
+    let as  := qsortAux lt as low mid;
+    qsortAux lt as (mid+1) high
   else as
 
 @[inline] def qsort {α : Type} [Inhabited α] (as : Array α) (lt : α → α → Bool) : Array α :=
diff --git a/tests/bench/rbmap.lean b/tests/bench/rbmap.lean
index ec624b2602..d0fdb26f34 100644
--- a/tests/bench/rbmap.lean
+++ b/tests/bench/rbmap.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -23,7 +24,7 @@ open color Nat Tree
 
 def fold (f : Nat → Bool → σ → σ) : Tree → σ → σ
 | Leaf, b               => b
-| Node _ l k v r,     b => fold r (f k v (fold l b))
+| Node _ l k v r,     b => fold f r (f k v (fold f l b))
 
 @[inline]
 def balance1 : Nat → Bool → Tree → Tree → Tree
diff --git a/tests/bench/rbmap_checkpoint.lean b/tests/bench/rbmap_checkpoint.lean
index 46a5a0f672..7b2433d0a5 100644
--- a/tests/bench/rbmap_checkpoint.lean
+++ b/tests/bench/rbmap_checkpoint.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -25,7 +26,7 @@ open color Nat Tree
 
 def fold (f : Nat → Bool → σ → σ) : Tree → σ → σ
 | Leaf, b               => b
-| Node _ l k v r,     b => fold r (f k v (fold l b))
+| Node _ l k v r,     b => fold f r (f k v (fold f l b))
 
 @[inline]
 def balance1 : Nat → Bool → Tree → Tree → Tree
@@ -72,7 +73,7 @@ def mkMapAux (freq : Nat) : Nat → Tree → List Tree → List Tree
 | n+1,   m, r =>
   let m := insert m n (n % 10 = 0);
   let r := if n % freq == 0 then m::r else r;
-  mkMapAux n m r
+  mkMapAux freq n m r
 
 def mkMap (n : Nat) (freq : Nat) : List Tree :=
 mkMapAux freq n Leaf []
@@ -83,7 +84,7 @@ def myLen : List Tree → Nat → Nat
 | [], r => r
 
 def main (xs : List String) : IO UInt32 := do
-[n, freq] ← pure xs | throw $ IO.userError "invalid input";
+let [n, freq] ← pure xs | throw $ IO.userError "invalid input";
 let n     := n.toNat!;
 let freq  := freq.toNat!;
 let freq  := if freq == 0 then 1 else freq;
diff --git a/tests/bench/unionfind.lean b/tests/bench/unionfind.lean
index cfc91e9225..a83f11e043 100644
--- a/tests/bench/unionfind.lean
+++ b/tests/bench/unionfind.lean
@@ -1,8 +1,9 @@
+#lang lean4
 def StateT' (m : Type → Type) (σ : Type) (α : Type) := σ → m (α × σ)
 namespace StateT'
 variables {m : Type → Type} [Monad m] {σ : Type} {α β : Type}
 @[inline] protected def pure (a : α) : StateT' m σ α := fun s => pure (a, s)
-@[inline] protected def bind (x : StateT' m σ α) (f : α → StateT' m σ β) : StateT' m σ β := fun s => do (a, s') ← x s; f a s'
+@[inline] protected def bind (x : StateT' m σ α) (f : α → StateT' m σ β) : StateT' m σ β := fun s => do let (a, s') ← x s; f a s'
 @[inline] def read : StateT' m σ σ := fun s => pure (s, s)
 @[inline] def write (s' : σ) : StateT' m σ Unit := fun s => pure ((), s')
 @[inline] def updt (f : σ → σ) : StateT' m σ Unit := fun s => pure ((), f s)
@@ -15,11 +16,11 @@ namespace ExceptT'
 variables {m : Type → Type} [Monad m] {ε : Type} {α β : Type}
 @[inline] protected def pure (a : α) : ExceptT' m ε α := (pure (Except.ok a) : m (Except ε α))
 @[inline] protected def bind (x : ExceptT' m ε α) (f : α → ExceptT' m ε β) : ExceptT' m ε β :=
-(do { v ← x; match v with
+(do { let v ← x; match v with
        | Except.error e => pure (Except.error e)
        | Except.ok a    => f a } : m (Except ε β))
 @[inline] def error (e : ε) : ExceptT' m ε α := (pure (Except.error e) : m (Except ε α))
-@[inline] def lift (x : m α) : ExceptT' m ε α := (do {a ← x; pure (Except.ok a) } : m (Except ε α))
+@[inline] def lift (x : m α) : ExceptT' m ε α := (do {let a ← x; pure (Except.ok a) } : m (Except ε α))
 instance : Monad (ExceptT' m ε) :=
 {pure := @ExceptT'.pure _ _ _, bind := @ExceptT'.bind _ _ _}
 end ExceptT'
@@ -40,35 +41,35 @@ def run {α : Type} (x : M α) (s : ufData := ∅) : Except String α × ufData
 x s
 
 def capacity : M Nat :=
-do d ← read; pure d.size
+do let d ← read; pure d.size
 
 def findEntryAux : Nat → Node → M nodeData
 | 0,   n => error "out of fuel"
 | i+1, n =>
-  do s ← read;
+  do let s ← read;
      if h : n < s.size then
        do { let e := s.get ⟨n, h⟩;
             if e.find = n then pure e
-            else do e₁ ← findEntryAux i e.find;
+            else do let e₁ ← findEntryAux i e.find;
                     updt (fun s => s.set! n e₁);
                     pure e₁ }
      else error "invalid Node"
 
 def findEntry (n : Node) : M nodeData :=
-do c ← capacity;
+do let c ← capacity;
    findEntryAux c n
 
 def find (n : Node) : M Node :=
-do e ← findEntry n; pure e.find
+do let e ← findEntry n; pure e.find
 
 def mk : M Node :=
-do n ← capacity;
+do let n ← capacity;
    updt $ fun s => s.push {find := n, rank := 1};
    pure n
 
 def union (n₁ n₂ : Node) : M Unit :=
-do r₁ ← findEntry n₁;
-   r₂ ← findEntry n₂;
+do let r₁ ← findEntry n₁;
+   let r₂ ← findEntry n₂;
    if r₁.find = r₂.find then pure ()
    else updt $ fun s =>
      if r₁.rank < r₂.rank then s.set! r₁.find { find := r₂.find }
@@ -83,30 +84,30 @@ def mkNodes : Nat → M Unit
 | n+1 => do _ ← mk; mkNodes n
 
 def checkEq (n₁ n₂ : Node) : M Unit :=
-do r₁ ← find n₁; r₂ ← find n₂;
-   unless (r₁ = r₂) $ error "nodes are not equal"
+do let r₁ ← find n₁; let r₂ ← find n₂;
+   unless (r₁ = r₂) do error "nodes are not equal"
 
 def mergePackAux : Nat → Nat → Nat → M Unit
 | 0,   _, _ => pure ()
-| i+1, n, d =>
-  do c ← capacity;
+| i+1, n, d => do
+  let c ← capacity;
   if (n+d) < c
   then union n (n+d) *> mergePackAux i (n+1) d
   else pure ()
 
 def mergePack (d : Nat) : M Unit :=
-do c ← capacity; mergePackAux c 0 d
+do let c ← capacity; mergePackAux c 0 d
 
 def numEqsAux : Nat → Node → Nat → M Nat
 | 0,   _, r => pure r
 | i+1, n, r =>
-  do c ← capacity;
+  do let c ← capacity;
      if n < c
-     then do { n₁ ← find n; numEqsAux i (n+1) (if n = n₁ then r else r+1) }
+     then do { let n₁ ← find n; numEqsAux i (n+1) (if n = n₁ then r else r+1) }
      else pure r
 
 def numEqs : M Nat :=
-do c ← capacity;
+do let c ← capacity;
    numEqsAux c 0 0
 
 def test (n : Nat) : M Nat :=
diff --git a/tests/compiler/foreign/README.md b/tests/compiler/foreign/README.md
index 90a1a77156..b3829a0114 100644
--- a/tests/compiler/foreign/README.md
+++ b/tests/compiler/foreign/README.md
@@ -6,7 +6,7 @@ The file `main.lean` contains a small Lean program that uses the exported primit
 Build instructions
 =====
 
-Assuming the Lean `bin/` directory (e.g. from `build/release/stage0.5`) is in your `PATH`,
+Assuming the Lean `bin/` directory (e.g. from `build/release/stage1`) is in your `PATH`,
 executing `leanmake` will create the executable `build/bin/test`.
 
 The executable `build/bin/test` should produce the output
diff --git a/tests/compiler/foreign/main.lean b/tests/compiler/foreign/main.lean
index 174caa9309..bc559a5d60 100644
--- a/tests/compiler/foreign/main.lean
+++ b/tests/compiler/foreign/main.lean
@@ -1,4 +1,5 @@
-constant SPointed : PointedType := arbitrary _
+#lang lean4
+constant SPointed : PointedType
 def S : Type := SPointed.type
 instance : Inhabited S := ⟨SPointed.val⟩
 
diff --git a/tests/compiler/print_error.lean b/tests/compiler/print_error.lean
index fd8be3803a..4e2e6b2005 100644
--- a/tests/compiler/print_error.lean
+++ b/tests/compiler/print_error.lean
@@ -1,3 +1,4 @@
+#lang lean4
 prelude
 import Init.System.IO
 
diff --git a/tests/compiler/reusebug.lean b/tests/compiler/reusebug.lean
index 1d02a11a5e..66419a8254 100644
--- a/tests/compiler/reusebug.lean
+++ b/tests/compiler/reusebug.lean
@@ -1,3 +1,4 @@
+#lang lean4
 inductive Expr
 | Val : Int → Expr
 | Var : String → Expr
@@ -6,7 +7,7 @@ inductive Expr
 
 open Expr
 
-def Expr.toString : Expr → String
+protected def Expr.toString : Expr → String
 | Val n   => toString n
 | Var x   => x
 | Add f g   => "(" ++ Expr.toString f ++ " + " ++ Expr.toString g ++ ")"
diff --git a/tests/compiler/str.lean b/tests/compiler/str.lean
index 1ab37b21f7..43696454f9 100644
--- a/tests/compiler/str.lean
+++ b/tests/compiler/str.lean
@@ -1,7 +1,8 @@
+#lang lean4
 def showChars : Nat → String → String.Pos → IO Unit
 | 0,     _, _   => pure ()
-| n+1,   s, idx =>
-  unless (s.atEnd idx) $
+| n+1,   s, idx => do
+  unless s.atEnd idx  do
     IO.println (">> " ++ toString (s.get idx)) *>
     showChars n s (s.next idx)
 
diff --git a/tests/compiler/t2.lean b/tests/compiler/t2.lean
index f40523bb45..90fdaf18e5 100644
--- a/tests/compiler/t2.lean
+++ b/tests/compiler/t2.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /- Benchmark for new code generator -/
 inductive Expr
 | Val : Int → Expr
@@ -52,10 +53,10 @@ def ln : Expr → Expr
 def d (x : String) : Expr → Expr
 | Val _     => Val 0
 | Var y     => if x = y then Val 1 else Val 0
-| Add f g   => add (d f) (d g)
-| Mul f g   => add (mul f (d g)) (mul g (d f))
-| Pow f g   => mul (pow f g) (add (mul (mul g (d f)) (pow f (Val (-1)))) (mul (ln f) (d g)))
-| Ln f      => mul (d f) (pow f (Val (-1)))
+| Add f g   => add (d x f) (d x g)
+| Mul f g   => add (mul f (d x g)) (mul g (d x f))
+| Pow f g   => mul (pow f g) (add (mul (mul g (d x f)) (pow f (Val (-1)))) (mul (ln f) (d x g)))
+| Ln f      => mul (d x f) (pow f (Val (-1)))
 
 def count : Expr → Nat
 | Val _   => 1
@@ -65,7 +66,7 @@ def count : Expr → Nat
 | Pow f g   => count f + count g
 | Ln f      => count f
 
-def Expr.toString : Expr → String
+protected def Expr.toString : Expr → String
 | Val n   => toString n
 | Var x   => x
 | Add f g   => "(" ++ Expr.toString f ++ " + " ++ Expr.toString g ++ ")"
@@ -78,7 +79,7 @@ instance : HasToString Expr :=
 
 def nestAux (s : Nat) (f : Nat → Expr → IO Expr) : Nat → Expr → IO Expr
 | 0,       x => pure x
-| m@(n+1), x => f (s - m) x >>= nestAux n
+| m@(n+1), x => f (s - m) x >>= nestAux s f n
 
 def nest (f : Nat → Expr → IO Expr) (n : Nat) (e : Expr) : IO Expr :=
 nestAux n f n e
diff --git a/tests/compiler/t4.lean b/tests/compiler/t4.lean
index 1931e935ae..5aa9211fac 100644
--- a/tests/compiler/t4.lean
+++ b/tests/compiler/t4.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /- Benchmark for new code generator -/
 inductive Expr
 | Val : Int → Expr
@@ -9,7 +10,7 @@ inductive Expr
 
 open Expr
 
-def Expr.toString : Expr → String
+protected def Expr.toString : Expr → String
 | Val n   => toString n
 | Var x   => x
 | Add f g   => "(" ++ Expr.toString f ++ " + " ++ Expr.toString g ++ ")"
@@ -73,12 +74,12 @@ def ln : Expr → Expr
 def d (x : String) : Expr → Expr
 | Val _     => Val 0
 | Var y     => if x = y then Val 1 else Val 0
-| Add f g   => add (d f) (d g)
+| Add f g   => add (d x f) (d x g)
 | Mul f g   =>
   -- dbgTrace (">> d (" ++ toString f ++ ", " ++ toString g ++ ")") $ fun _ =>
-  add (mul f (d g)) (mul g (d f))
-| Pow f g   => mul (pow f g) (add (mul (mul g (d f)) (pow f (Val (-1)))) (mul (ln f) (d g)))
-| Ln f      => mul (d f) (pow f (Val (-1)))
+  add (mul f (d x g)) (mul g (d x f))
+| Pow f g   => mul (pow f g) (add (mul (mul g (d x f)) (pow f (Val (-1)))) (mul (ln f) (d x g)))
+| Ln f      => mul (d x f) (pow f (Val (-1)))
 
 def count : Expr → Nat
 | Val _   => 1
@@ -91,7 +92,7 @@ def count : Expr → Nat
 
 def nestAux (s : Nat) (f : Nat → Expr → IO Expr) : Nat → Expr → IO Expr
 | 0,       x => pure x
-| m@(n+1), x => f (s - m) x >>= nestAux n
+| m@(n+1), x => f (s - m) x >>= nestAux s f n
 
 def nest (f : Nat → Expr → IO Expr) (n : Nat) (e : Expr) : IO Expr :=
 nestAux n f n e
diff --git a/tests/compiler/thunk.lean b/tests/compiler/thunk.lean
index 2b80fe043b..80f5cbe31a 100644
--- a/tests/compiler/thunk.lean
+++ b/tests/compiler/thunk.lean
@@ -1,3 +1,4 @@
+#lang lean4
 def compute (v : Nat) : Thunk Nat :=
 ⟨fun _ => let xs := List.replicate 100000 v; xs.foldl Nat.add 0⟩
 
diff --git a/tests/compiler/uint_fold.lean b/tests/compiler/uint_fold.lean
index c989d63e6c..e8326fc7bb 100644
--- a/tests/compiler/uint_fold.lean
+++ b/tests/compiler/uint_fold.lean
@@ -1,5 +1,6 @@
-@[noinline]
-def h (x : Nat) : UInt32 :=
+#lang lean4
+
+@[noinline] def h (x : Nat) : UInt32 :=
 UInt32.ofNat x
 
 def f (x y : UInt32) : UInt32 :=
@@ -9,7 +10,7 @@ let a2 : UInt32 := x + a1;
 let a3 : UInt32 := 10;
 y + a2 + h v + a3
 
-partial def g : UInt32 → UInt32 → UInt32 | x, y =>
+partial def g (x : UInt32) (y : UInt32) : UInt32 :=
 if x = 0 then y else g (x-1) (y+2)
 
 def foo : UInt8 :=
diff --git a/tests/lean/run/newfrontend1.lean b/tests/lean/run/newfrontend1.lean
index 0ae90a27e3..9e458a25fa 100644
--- a/tests/lean/run/newfrontend1.lean
+++ b/tests/lean/run/newfrontend1.lean
@@ -271,9 +271,6 @@ def altTst2 {m σ} [Alternative m] [Monad m] : Alternative (StateT σ m) :=
 def altTst3 {m σ} [Alternative m] [Monad m] : Alternative (StateT σ m) :=
 ⟨fun {α} => StateT.failure, fun {α} => StateT.orelse⟩
 
-def altTst4 {m σ} [Alternative m] [Monad m] : Alternative (StateT σ m) :=
-⟨@StateT.failure _ _ _ _, @StateT.orelse _ _ _ _⟩
-
 #check_failure 1 + true
 
 /-