diff --git a/tests/compiler/expr.lean b/tests/compiler/expr.lean
index 3be66f1ed1..30c712d644 100644
--- a/tests/compiler/expr.lean
+++ b/tests/compiler/expr.lean
@@ -3,7 +3,7 @@ open Lean
 
 def main : IO UInt32 :=
 do
-let e := Expr.app (Expr.app (Expr.const `f []) (Expr.const `a [])) (Expr.const `b []);
+let e := mkAppN (mkConst `f) #[mkConst `a, mkConst `b];
 IO.println e;
 IO.println ("hash: " ++ toString e.hash);
 IO.println e.getAppArgs;
diff --git a/tests/lean/abst.lean b/tests/lean/abst.lean
index 6df62d3454..d0bb3646f0 100644
--- a/tests/lean/abst.lean
+++ b/tests/lean/abst.lean
@@ -4,21 +4,21 @@ open Lean
 def tst : IO Unit :=
 do
 let f := mkConst `f;
-let x := Expr.fvar `x;
-let y := Expr.fvar `y;
-let t := Expr.app (Expr.app (Expr.app f x) y) (Expr.app f x);
-IO.println t.dbgToString;
+let x := mkFVar `x;
+let y := mkFVar `y;
+let t := mkApp (mkApp (mkApp f x) y) (mkApp f x);
+IO.println t;
 let p := t.abstract [x, y].toArray;
-IO.println p.dbgToString;
-IO.println (p.instantiateRev [x, y].toArray).dbgToString;
+IO.println p;
+IO.println $ p.instantiateRev #[x, y];
 let a := mkConst `a;
-let b := Expr.app f (mkConst `b);
-IO.println (p.instantiateRev [a, b].toArray).dbgToString;
-IO.println (p.instantiate [a].toArray).dbgToString;
-let p := t.abstractRange 1 [x, y].toArray;
-IO.println p.dbgToString;
-let p := t.abstractRange 3 [x, y].toArray;
-IO.println p.dbgToString;
+let b := mkApp f (mkConst `b);
+IO.println $ p.instantiateRev #[a, b];
+IO.println $ p.instantiate #[a];
+let p := t.abstractRange 1 #[x, y];
+IO.println p;
+let p := t.abstractRange 3 #[x, y];
+IO.println p;
 pure ()
 
 #eval tst
diff --git a/tests/lean/inst.lean b/tests/lean/inst.lean
index f8e77050ec..6f20b2a980 100644
--- a/tests/lean/inst.lean
+++ b/tests/lean/inst.lean
@@ -4,11 +4,11 @@ open Lean
 def tst : IO Unit :=
 do
 let f := mkConst `f;
-let x := Expr.bvar 0;
-let y := Expr.bvar 1;
-let t := Expr.app (Expr.app (Expr.app f x) y) x;
+let x := mkBVar 0;
+let y := mkBVar 1;
+let t := mkApp (mkApp (mkApp f x) y) x;
 let a := mkConst `a;
-let b := Expr.app f (mkConst `b);
+let b := mkApp f (mkConst `b);
 let c := mkConst `c;
 IO.println t;
 IO.println (t.instantiate #[a, b]);
diff --git a/tests/lean/mvar1.lean b/tests/lean/mvar1.lean
index 6a2cfa05ed..4a8336017b 100644
--- a/tests/lean/mvar1.lean
+++ b/tests/lean/mvar1.lean
@@ -35,8 +35,7 @@ def m5 := mkMVar `m5
 def m6 := mkMVar `m6
 
 def bi := BinderInfo.default
-def arrow (d b : Expr) := Expr.forallE `_ bi d b
-
+def arrow (d b : Expr) := mkForall `_ bi d b
 def lctx1 : LocalContext := {}
 def lctx2 := lctx1.mkLocalDecl `α `α typeE
 def lctx3 := lctx2.mkLocalDecl `x `x natE
@@ -44,7 +43,7 @@ def lctx4 := lctx3.mkLocalDecl `y `y α
 def lctx5 := lctx4.mkLocalDecl `z `z (mkAppN vecE #[x])
 def lctx6 := lctx5.mkLocalDecl `w `w (arrow natE (mkAppN m6 #[α, x, y]))
 
-def t1 := lctx5.mkLambda #[α, x, y] $ mkAppN f #[α, mkAppN g #[x, y], lctx5.mkLambda #[z] (Expr.app f z)]
+def t1 := lctx5.mkLambda #[α, x, y] $ mkAppN f #[α, mkAppN g #[x, y], lctx5.mkLambda #[z] (mkApp f z)]
 #eval check (!t1.hasFVar)
 #eval t1
 
diff --git a/tests/lean/mvar2.lean b/tests/lean/mvar2.lean
index a3fcd5c790..b33e24ee44 100644
--- a/tests/lean/mvar2.lean
+++ b/tests/lean/mvar2.lean
@@ -16,7 +16,7 @@ def b2 := mkBVar 2
 
 def u := Level.param `u
 
-def typeE := Expr.sort Level.one
+def typeE := mkSort Level.one
 def natE  := mkConst `Nat []
 def boolE := mkConst `Bool []
 def vecE  := mkConst `Vec [Level.zero]
@@ -32,7 +32,7 @@ def m2 := mkMVar `m2
 def m3 := mkMVar `m3
 
 def bi := BinderInfo.default
-def arrow (d b : Expr) := Expr.forallE `_ bi d b
+def arrow (d b : Expr) := mkForall `_ bi d b
 
 def lctx1 : LocalContext := {}
 def lctx2 := lctx1.mkLocalDecl `α `α typeE
diff --git a/tests/lean/mvar3.lean b/tests/lean/mvar3.lean
index bb0e62ef0d..011d693ee4 100644
--- a/tests/lean/mvar3.lean
+++ b/tests/lean/mvar3.lean
@@ -1,7 +1,7 @@
 import Init.Lean.MetavarContext
 open Lean
 
-def mkLambda (mctx : MetavarContext) (ngen : NameGenerator) (lctx : LocalContext) (xs : Array Expr) (e : Expr)
+def mkLambdaTest (mctx : MetavarContext) (ngen : NameGenerator) (lctx : LocalContext) (xs : Array Expr) (e : Expr)
     : Except MetavarContext.MkBinding.Exception (MetavarContext × NameGenerator × Expr) :=
 match MetavarContext.mkLambda xs e lctx { mctx := mctx, ngen := ngen } with
 | EStateM.Result.ok e s    => Except.ok (s.mctx, s.ngen, e)
@@ -22,7 +22,7 @@ def b2 := mkBVar 2
 
 def u := Level.param `u
 
-def typeE := Expr.sort Level.one
+def typeE := mkSort Level.one
 def natE  := mkConst `Nat
 def boolE := mkConst `Bool
 def vecE  := mkConst `Vec [Level.zero]
@@ -33,12 +33,12 @@ def y := mkFVar `y
 def z := mkFVar `z
 def w := mkFVar `w
 
-def m1 := Expr.mvar `m1
-def m2 := Expr.mvar `m2
-def m3 := Expr.mvar `m3
+def m1 := mkMVar `m1
+def m2 := mkMVar `m2
+def m3 := mkMVar `m3
 
 def bi := BinderInfo.default
-def arrow (d b : Expr) := Expr.forallE `_ bi d b
+def arrow (d b : Expr) := mkForall `_ bi d b
 
 def lctx1 : LocalContext := {}
 def lctx2 := lctx1.mkLocalDecl `α `α typeE
@@ -52,7 +52,7 @@ def mctx4  := mctx3.addExprMVarDecl `m3 `m3 lctx3 natE
 def mctx4' := mctx3.addExprMVarDecl `m3 `m3 lctx3 natE true
 
 def R1 :=
-match mkLambda mctx4 {namePrefix := `n} lctx4 #[α, x, y] $ mkAppN f #[m3, x] with
+match mkLambdaTest mctx4 {namePrefix := `n} lctx4 #[α, x, y] $ mkAppN f #[m3, x] with
 | Except.ok s    => s
 | Except.error e => panic! (toString e)
 def e1    := R1.2.2
@@ -64,7 +64,7 @@ def mctx5 := R1.1
 #eval check (!e1.hasFVar)
 
 def R2 :=
-match mkLambda mctx4' {namePrefix := `n} lctx4 #[α, x, y] $ mkAppN f #[m3, y] with
+match mkLambdaTest mctx4' {namePrefix := `n} lctx4 #[α, x, y] $ mkAppN f #[m3, y] with
 | Except.ok s    => s
 | Except.error e => panic! (toString e)
 def e2    := R2.2.2
@@ -79,7 +79,7 @@ def mctx6 := R2.1
 #print "assigning ?m1 and ?n.1"
 def R3 :=
 let mctx := mctx6.assignExpr `m3 x;
-let mctx := mctx.assignExpr (Name.mkNumeral `n 1) (Expr.lam `_ bi typeE natE);
+let mctx := mctx.assignExpr (Name.mkNumeral `n 1) (mkLambda `_ bi typeE natE);
 -- ?n.2 is instantiated because we have the delayed assignment `?n.2 α x := ?m1`
 (mctx.instantiateMVars e2)
 def e3    := R3.1
diff --git a/tests/lean/mvar_fvar.lean b/tests/lean/mvar_fvar.lean
index 373d9aa849..39d9c99386 100644
--- a/tests/lean/mvar_fvar.lean
+++ b/tests/lean/mvar_fvar.lean
@@ -1,10 +1,10 @@
 import Init.Lean
 open Lean
 
-#eval (Expr.fvar `a).hasFVar
-#eval (Expr.app (Expr.const `foo []) (Expr.fvar `a)).hasFVar
-#eval (Expr.app (Expr.const `foo []) (Expr.const `a [])).hasFVar
+#eval (mkFVar `a).hasFVar
+#eval (mkApp (mkConst `foo) (mkFVar `a)).hasFVar
+#eval (mkApp (mkConst `foo) (mkConst `a)).hasFVar
 
-#eval (Expr.mvar `a).hasMVar
-#eval (Expr.app (Expr.const `foo []) (Expr.mvar `a)).hasMVar
-#eval (Expr.app (Expr.const `foo []) (Expr.const `a [])).hasMVar
+#eval (mkMVar `a).hasMVar
+#eval (mkApp (mkConst `foo) (mkMVar `a)).hasMVar
+#eval (mkApp (mkConst `foo) (mkConst `a)).hasMVar
diff --git a/tests/lean/run/expr1.lean b/tests/lean/run/expr1.lean
index e3c13a5f80..a749904626 100644
--- a/tests/lean/run/expr1.lean
+++ b/tests/lean/run/expr1.lean
@@ -47,8 +47,8 @@ do let f   := mkConst `f [];
    let x1   := mkBVar 1;
    let t1   := mkAppN f #[a, b];
    let t2   := mkAppN f #[a, x0];
-   let t3   := Expr.lam `x BinderInfo.default (Expr.sort Level.zero) (mkAppN f #[a, x0]);
-   let t4   := Expr.lam `x BinderInfo.default (Expr.sort Level.zero) (mkAppN f #[a, x1]);
+   let t3   := mkLambda `x BinderInfo.default (mkSort Level.zero) (mkAppN f #[a, x0]);
+   let t4   := mkLambda `x BinderInfo.default (mkSort Level.zero) (mkAppN f #[a, x1]);
    unless (!t1.hasLooseBVar 0) $ throw "failed-1";
    unless (t2.hasLooseBVar 0) $ throw "failed-2";
    unless (!t3.hasLooseBVar 0) $ throw "failed-3";
@@ -66,29 +66,29 @@ do let f   := mkConst `f [];
    let x0  := mkBVar 0;
    let x1  := mkBVar 1;
    let x2  := mkBVar 2;
-   let t   := Expr.lam `x BinderInfo.default nat (Expr.app f x0);
+   let t   := mkLambda `x BinderInfo.default nat (mkApp f x0);
    IO.println t.etaExpanded?;
    unless (t.etaExpanded? == some f) $ throw "failed-1";
-   let t   := Expr.lam `x BinderInfo.default nat (Expr.app f x1);
+   let t   := mkLambda `x BinderInfo.default nat (mkApp f x1);
    unless (t.etaExpanded? == none) $ throw "failed-2";
-   let t   := Expr.lam `x BinderInfo.default nat (mkAppN f #[a, x0]);
-   unless (t.etaExpanded? == some (Expr.app f a)) $ throw "failed-3";
-   let t   := Expr.lam `x BinderInfo.default nat (mkAppN f #[x0, x0]);
+   let t   := mkLambda `x BinderInfo.default nat (mkAppN f #[a, x0]);
+   unless (t.etaExpanded? == some (mkApp f a)) $ throw "failed-3";
+   let t   := mkLambda `x BinderInfo.default nat (mkAppN f #[x0, x0]);
    unless (t.etaExpanded? == none) $ throw "failed-4";
-   let t   := Expr.lam `x BinderInfo.default nat (Expr.lam `y BinderInfo.default nat (Expr.app f x0));
+   let t   := mkLambda `x BinderInfo.default nat (mkLambda `y BinderInfo.default nat (mkApp f x0));
    unless (t.etaExpanded? == none) $ throw "failed-5";
-   let t   := Expr.lam `x BinderInfo.default nat (Expr.lam `y BinderInfo.default nat (mkAppN f #[x1, x0]));
+   let t   := mkLambda `x BinderInfo.default nat (mkLambda `y BinderInfo.default nat (mkAppN f #[x1, x0]));
    IO.println t;
    unless (t.etaExpanded? == some f) $ throw "failed-6";
-   let t   := Expr.lam `x BinderInfo.default nat (Expr.lam `y BinderInfo.default nat (Expr.lam `z BinderInfo.default nat (mkAppN f #[x2, x1, x0])));
+   let t   := mkLambda `x BinderInfo.default nat (mkLambda `y BinderInfo.default nat (mkLambda `z BinderInfo.default nat (mkAppN f #[x2, x1, x0])));
    IO.println t;
    unless (t.etaExpanded? == some f) $ throw "failed-7";
-   let t   := Expr.lam `x BinderInfo.default nat (Expr.lam `y BinderInfo.default nat (Expr.lam `z BinderInfo.default nat (mkAppN f #[a, x2, x1, x0])));
+   let t   := mkLambda `x BinderInfo.default nat (mkLambda `y BinderInfo.default nat (mkLambda `z BinderInfo.default nat (mkAppN f #[a, x2, x1, x0])));
    IO.println t;
-   unless (t.etaExpanded? == some (Expr.app f a)) $ throw "failed-8";
+   unless (t.etaExpanded? == some (mkApp f a)) $ throw "failed-8";
    IO.println t.etaExpanded?;
-   let t   := Expr.app f a;
-   unless (t.etaExpanded? == some (Expr.app f a)) $ throw "failed-9";
+   let t   := mkApp f a;
+   unless (t.etaExpanded? == some (mkApp f a)) $ throw "failed-9";
    pure ()
 
 #eval tst5
diff --git a/tests/lean/run/expr_maps.lean b/tests/lean/run/expr_maps.lean
index f17595382a..409db80501 100644
--- a/tests/lean/run/expr_maps.lean
+++ b/tests/lean/run/expr_maps.lean
@@ -1,21 +1,21 @@
 import Init.Lean.Expr
 open Lean
 
-def exprType : Expr := Expr.sort Level.one
+def exprType : Expr := mkSort Level.one
 def biDef           := BinderInfo.default
-def exprNat         := Expr.const `Nat []
+def exprNat         := mkConst `Nat []
 -- Type -> Type
-def TypeArrowType   := Expr.forallE `α biDef exprType exprType
+def TypeArrowType   := mkForall `α biDef exprType exprType
 -- Type -> Type
-def TypeArrowType2  := Expr.forallE `β biDef exprType exprType
--- fun (x : Nat), x
-def exprT1          := Expr.lam `x biDef exprNat (Expr.bvar 0)
--- fun (y : Nat), x
-def exprT2          := Expr.lam `y biDef exprNat (Expr.bvar 0)
--- fun (x : Nat), (f x)
-def exprT3          := Expr.lam `x biDef exprNat (Expr.app (Expr.const `f []) (Expr.bvar 0))
--- fun (x : Nat), (f x)
-def exprT4          := Expr.lam `x BinderInfo.implicit exprNat (Expr.app (Expr.const `f []) (Expr.bvar 0))
+def TypeArrowType2  := mkForall `β biDef exprType exprType
+-- fun (x : Nat) => x
+def exprT1          := mkLambda `x biDef exprNat (mkBVar 0)
+-- fun (y : Nat) => x
+def exprT2          := mkLambda `y biDef exprNat (mkBVar 0)
+-- fun (x : Nat) => (f x)
+def exprT3          := mkLambda `x biDef exprNat (mkApp (mkConst `f []) (mkBVar 0))
+-- fun (x : Nat) => (f x)
+def exprT4          := mkLambda `x BinderInfo.implicit exprNat (mkApp (mkConst `f []) (mkBVar 0))
 
 def check (b : Bool) : IO Unit :=
 unless b (throw "failed")
diff --git a/tests/lean/run/meta1.lean b/tests/lean/run/meta1.lean
index 2b7b896e8a..d48487bb16 100644
--- a/tests/lean/run/meta1.lean
+++ b/tests/lean/run/meta1.lean
@@ -29,30 +29,30 @@ mkAppN map #[nat, bool]
 #eval tstInferType [`Init.Data.List] t1
 
 def t2 : Expr :=
-let prop := Expr.sort Level.zero;
-Expr.forallE `x BinderInfo.default prop prop
+let prop := mkSort Level.zero;
+mkForall `x BinderInfo.default prop prop
 
 #eval tstInferType [`Init.Core] t2
 
 def t3 : Expr :=
 let nat   := mkConst `Nat [];
 let natLe := mkConst `Nat.le [];
-let zero  := Expr.lit (Literal.natVal 0);
-let p     := mkAppN natLe #[Expr.bvar 0, zero];
-Expr.forallE `x BinderInfo.default nat p
+let zero  := mkLit (Literal.natVal 0);
+let p     := mkAppN natLe #[mkBVar 0, zero];
+mkForall `x BinderInfo.default nat p
 
 #eval tstInferType [`Init.Data.Nat] t3
 
 def t4 : Expr :=
 let nat   := mkConst `Nat [];
-let p     := mkAppN (mkConst `Nat.succ []) #[Expr.bvar 0];
-Expr.lam `x BinderInfo.default nat p
+let p     := mkAppN (mkConst `Nat.succ []) #[mkBVar 0];
+mkLambda `x BinderInfo.default nat p
 
 #eval tstInferType [`Init.Core] t4
 
 def t5 : Expr :=
 let add   := mkConst `Nat.add [];
-mkAppN add #[Expr.lit (Literal.natVal 3), Expr.lit (Literal.natVal 5)]
+mkAppN add #[mkLit (Literal.natVal 3), mkLit (Literal.natVal 5)]
 
 #eval tstWHNF [`Init.Data.Nat] t5
 #eval tstWHNF [`Init.Data.Nat] t5 TransparencyMode.reducible
@@ -64,58 +64,58 @@ def t6 : Expr :=
 let map  := mkConst `List.map [Level.one, Level.one];
 let nat  := mkConst `Nat [];
 let add  := mkConst `Nat.add [];
-let f    := Expr.lam `x BinderInfo.default nat (mkAppN add #[Expr.bvar 0, Expr.lit (Literal.natVal 1)]);
-let cons := Expr.app (mkConst `List.cons [Level.zero]) nat;
-let nil  := Expr.app (mkConst `List.nil [Level.zero]) nat;
-let one  := Expr.lit (Literal.natVal 1);
-let four := Expr.lit (Literal.natVal 4);
-let xs   := Expr.app (Expr.app cons one) (Expr.app (Expr.app cons four) nil);
+let f    := mkLambda `x BinderInfo.default nat (mkAppN add #[mkBVar 0, mkLit (Literal.natVal 1)]);
+let cons := mkApp (mkConst `List.cons [Level.zero]) nat;
+let nil  := mkApp (mkConst `List.nil [Level.zero]) nat;
+let one  := mkLit (Literal.natVal 1);
+let four := mkLit (Literal.natVal 4);
+let xs   := mkApp (mkApp cons one) (mkApp (mkApp cons four) nil);
 mkAppN map #[nat, nat, f, xs]
 
 #eval tstInferType [`Init.Data.List] t6
 #eval tstWHNF [`Init.Data.List] t6
 
-#eval tstInferType [] $ Expr.sort Level.zero
+#eval tstInferType [] $ mkSort Level.zero
 
-#eval tstInferType [`Init.Data.List] $ Expr.lam `a BinderInfo.implicit (Expr.sort Level.one) (Expr.lam `x BinderInfo.default (Expr.bvar 0) (Expr.lam `xs BinderInfo.default (Expr.app (mkConst `List [Level.zero]) (Expr.bvar 1)) (Expr.bvar 0)))
+#eval tstInferType [`Init.Data.List] $ mkLambda `a BinderInfo.implicit (mkSort Level.one) (mkLambda `x BinderInfo.default (mkBVar 0) (mkLambda `xs BinderInfo.default (mkApp (mkConst `List [Level.zero]) (mkBVar 1)) (mkBVar 0)))
 
 def t7 : Expr :=
 let nat  := mkConst `Nat [];
-let one  := Expr.lit (Literal.natVal 1);
-Expr.letE `x nat one one
+let one  := mkLit (Literal.natVal 1);
+mkLet `x nat one one
 
 #eval tstInferType [`Init.Core] $ t7
 #eval tstWHNF [`Init.Core] $ t7
 
 def t8 : Expr :=
 let nat  := mkConst `Nat [];
-let one  := Expr.lit (Literal.natVal 1);
+let one  := mkLit (Literal.natVal 1);
 let add  := mkConst `Nat.add [];
-Expr.letE `x nat one (mkAppN add #[one, Expr.bvar 0])
+mkLet `x nat one (mkAppN add #[one, mkBVar 0])
 
 #eval tstInferType [`Init.Core] $ t8
 #eval tstWHNF [`Init.Core] $ t8
 
 def t9 : Expr :=
 let nat  := mkConst `Nat [];
-Expr.letE `a (Expr.sort Level.one) nat (Expr.forallE `x BinderInfo.default (Expr.bvar 0) (Expr.bvar 1))
+mkLet `a (mkSort Level.one) nat (mkForall `x BinderInfo.default (mkBVar 0) (mkBVar 1))
 
 #eval tstInferType [`Init.Core] $ t9
 #eval tstWHNF [`Init.Core] $ t9
 
-#eval tstInferType [`Init.Core] $ Expr.lit (Literal.natVal 10)
-#eval tstInferType [`Init.Core] $ Expr.lit (Literal.strVal "hello")
-#eval tstInferType [`Init.Core] $ Expr.mdata {} $ Expr.lit (Literal.natVal 10)
+#eval tstInferType [`Init.Core] $ mkLit (Literal.natVal 10)
+#eval tstInferType [`Init.Core] $ mkLit (Literal.strVal "hello")
+#eval tstInferType [`Init.Core] $ mkMData {} $ mkLit (Literal.natVal 10)
 
-#eval tstInferType [`Init.Lean.Trace] (Expr.proj `Inhabited 0 (mkConst `Lean.TraceState.Inhabited []))
-#eval tstInferType [`Init.Lean.Trace] (Expr.proj `Lean.TraceState 0 (Expr.proj `Inhabited 0 (mkConst `Lean.TraceState.Inhabited [])))
-#eval tstWHNF [`Init.Lean.Trace] (Expr.proj `Inhabited 0 (mkConst `Lean.TraceState.Inhabited []))
-#eval tstWHNF [`Init.Lean.Trace] (Expr.proj `Lean.TraceState 0 (Expr.proj `Inhabited 0 (mkConst `Lean.TraceState.Inhabited [])))
+#eval tstInferType [`Init.Lean.Trace] (mkProj `Inhabited 0 (mkConst `Lean.TraceState.Inhabited []))
+#eval tstInferType [`Init.Lean.Trace] (mkProj `Lean.TraceState 0 (mkProj `Inhabited 0 (mkConst `Lean.TraceState.Inhabited [])))
+#eval tstWHNF [`Init.Lean.Trace] (mkProj `Inhabited 0 (mkConst `Lean.TraceState.Inhabited []))
+#eval tstWHNF [`Init.Lean.Trace] (mkProj `Lean.TraceState 0 (mkProj `Inhabited 0 (mkConst `Lean.TraceState.Inhabited [])))
 
 def t10 : Expr :=
 let nat  := mkConst `Nat [];
-let refl := Expr.app (mkConst `Eq.refl [Level.one]) nat;
-Expr.lam `a BinderInfo.default nat (Expr.app refl (Expr.bvar 0))
+let refl := mkApp (mkConst `Eq.refl [Level.one]) nat;
+mkLambda `a BinderInfo.default nat (mkApp refl (mkBVar 0))
 
 #eval tstInferType [`Init.Core] t10
 #eval tstIsProp [`Init.Core] t10
@@ -125,17 +125,17 @@ Expr.lam `a BinderInfo.default nat (Expr.app refl (Expr.bvar 0))
 #eval tstIsProp [`Init.Core] (mkConst `And [])
 
 -- Example where isPropQuick fails
-#eval tstIsProp [`Init.Core] (mkAppN (mkConst `id [Level.zero]) #[Expr.sort Level.zero, mkAppN (mkConst `And []) #[mkConst `True [], mkConst
+#eval tstIsProp [`Init.Core] (mkAppN (mkConst `id [Level.zero]) #[mkSort Level.zero, mkAppN (mkConst `And []) #[mkConst `True [], mkConst
  `True []]])
 
-#eval tstIsProp [`Init.Core] (mkAppN (mkConst `Eq [Level.one]) #[mkConst `Nat [], Expr.lit (Literal.natVal 0), Expr.lit (Literal.natVal 1)])
+#eval tstIsProp [`Init.Core] (mkAppN (mkConst `Eq [Level.one]) #[mkConst `Nat [], mkLit (Literal.natVal 0), mkLit (Literal.natVal 1)])
 
 #eval tstIsProp [`Init.Core] $
-  Expr.forallE `x BinderInfo.default (mkConst `Nat [])
-    (mkAppN (mkConst `Eq [Level.one]) #[mkConst `Nat [], Expr.bvar 0, Expr.lit (Literal.natVal 1)])
+  mkForall `x BinderInfo.default (mkConst `Nat [])
+    (mkAppN (mkConst `Eq [Level.one]) #[mkConst `Nat [], mkBVar 0, mkLit (Literal.natVal 1)])
 
 #eval tstIsProp [`Init.Core] $
-  Expr.app
-    (Expr.lam `x BinderInfo.default (mkConst `Nat [])
-      (mkAppN (mkConst `Eq [Level.one]) #[mkConst `Nat [], Expr.bvar 0, Expr.lit (Literal.natVal 1)]))
-    (Expr.lit (Literal.natVal 0))
+  mkApp
+    (mkLambda `x BinderInfo.default (mkConst `Nat [])
+      (mkAppN (mkConst `Eq [Level.one]) #[mkConst `Nat [], mkBVar 0, mkLit (Literal.natVal 1)]))
+    (mkLit (Literal.natVal 0))
diff --git a/tests/lean/run/update.lean b/tests/lean/run/update.lean
index fa6b41f9ef..dbd7bdc3a4 100644
--- a/tests/lean/run/update.lean
+++ b/tests/lean/run/update.lean
@@ -2,28 +2,28 @@ import Init.Lean.Expr
 open Lean
 
 def main : IO Unit :=
-do let f   := Expr.const `f [];
-   let x   := Expr.const `x [];
-   let y   := Expr.const `y [];
-   let t1  := Expr.app f x;
+do let f   := mkConst `f [];
+   let x   := mkConst `x [];
+   let y   := mkConst `y [];
+   let t1  := mkApp f x;
    let t2  := t1.updateApp! f y;
    let t3  := t1.updateApp! f x;
-   let t4  := Expr.proj `Prod 1 x;
+   let t4  := mkProj `Prod 1 x;
    let t5  := t4.updateProj! y;
    let t6  := t4.updateProj! x;
    let x₁  := x.updateConst! [Level.one];
    let x₂  := x.updateConst! [];
-   let s   := Expr.sort Level.one;
+   let s   := mkSort Level.one;
    let s₁  := s.updateSort! Level.one;
    let s₂  := s.updateSort! Level.zero;
-   let a   := Expr.forallE `x BinderInfo.default s s;
+   let a   := mkForall `x BinderInfo.default s s;
    let a₁  := a.updateForall! BinderInfo.default s s;
    let a₂  := a.updateForall! BinderInfo.default s₂ s;
-   let nat := Expr.const `Nat [];
-   let id  := Expr.lam `x BinderInfo.default nat (Expr.bvar 0);
-   let id₁ := id.updateLambda! BinderInfo.default s (Expr.bvar 0);
-   let id₂ := id.updateLambda! BinderInfo.default nat (Expr.bvar 0);
-   let l   := Expr.letE `z nat x t1;
+   let nat := mkConst `Nat [];
+   let id  := mkLambda `x BinderInfo.default nat (mkBVar 0);
+   let id₁ := id.updateLambda! BinderInfo.default s (mkBVar 0);
+   let id₂ := id.updateLambda! BinderInfo.default nat (mkBVar 0);
+   let l   := mkLet `z nat x t1;
    let l₁  := l.updateLet! nat x t2;
    let l₂  := l.updateLet! nat x t1;
    IO.println [t1, t2, t3, t5, t6, x₁, x₂, s₁, s₂, a₁, a₂, id₁, id₂, l₁, l₂];
diff --git a/tests/lean/typeclass_context.lean b/tests/lean/typeclass_context.lean
index 788298bc69..128359a6ba 100644
--- a/tests/lean/typeclass_context.lean
+++ b/tests/lean/typeclass_context.lean
@@ -31,25 +31,25 @@ get >>= λ (ctx : Context) => pure $ ctx.eInstantiate t
 def testEUnify4 : EStateM String Context Expr := do
 t₁ ← EStateM.fromStateM $ eNewMeta (mkConst "Term");
 t₂ ← EStateM.fromStateM $ eNewMeta (mkConst "Term");
-eUnify (Expr.forallE "foo" BinderInfo.default t₂ t₁) (Expr.forallE "foo" BinderInfo.default t₁ t₂);
+eUnify (mkForall "foo" BinderInfo.default t₂ t₁) (mkForall "foo" BinderInfo.default t₁ t₂);
 get >>= λ (ctx : Context) => pure $ ctx.eInstantiate t₂
 
 def testEUnify5 : EStateM String Context Expr := do
 t₁ ← EStateM.fromStateM $ eNewMeta (mkConst "Term");
 t₂ ← EStateM.fromStateM $ eNewMeta (mkConst "Term");
-eUnify (Expr.forallE "foo" BinderInfo.default t₁ t₂) (Expr.forallE "foo" BinderInfo.default t₂ t₁);
+eUnify (mkForall "foo" BinderInfo.default t₁ t₂) (mkForall "foo" BinderInfo.default t₂ t₁);
 get >>= λ (ctx : Context) => pure $ ctx.eInstantiate t₂
 
 def testEUnify6 : EStateM String Context Expr := do
 u ← EStateM.fromStateM Context.uNewMeta;
-let t₁ := Expr.const "foo" [Level.zero];
-let t₂ := Expr.const "foo" [u];
+let t₁ := mkConst "foo" [Level.zero];
+let t₂ := mkConst "foo" [u];
 eUnify t₁ t₂;
 get >>= λ (ctx : Context) => pure $ ctx.eInstantiate t₂
 
 def testEUnify7 : EStateM String Context Expr := do
-e ← EStateM.fromStateM $ Context.eNewMeta $ Expr.sort Level.zero;
-let t₁ := Expr.fvar "foo";
+e ← EStateM.fromStateM $ Context.eNewMeta $ mkSort Level.zero;
+let t₁ := mkFVar "foo";
 let t₂ := e;
 eUnify t₁ t₂;
 get >>= λ (ctx : Context) => pure $ ctx.eInstantiate t₂
@@ -98,7 +98,7 @@ pure $ αNorm (mkConst "f")
 def testAlphaNorm4 : EStateM String Context Expr := do
 t₁ ← EStateM.fromStateM $ eNewMeta (mkConst "Term");
 t₂ ← EStateM.fromStateM $ eNewMeta (mkConst "Term");
-pure $ αNorm $ Expr.forallE "foo" BinderInfo.default (mkAppN (mkConst "f") #[t₂]) (mkAppN (mkConst "g") #[t₁])
+pure $ αNorm $ mkForall "foo" BinderInfo.default (mkAppN (mkConst "f") #[t₂]) (mkAppN (mkConst "g") #[t₁])
 
 #eval testEUnify1.run {}
 #eval testEUnify2.run {}
diff --git a/tests/playground/ir.lean b/tests/playground/ir.lean
index 2674a7ba81..8514077524 100644
--- a/tests/playground/ir.lean
+++ b/tests/playground/ir.lean
@@ -4,7 +4,7 @@ open Lean.IR
 def tst1 : IO Unit :=
 let fbody : FnBody :=
    FnBody.vdecl `x IRType.uint32 (Expr.lit (LitVal.num 0)) $
-   FnBody.ret `x in
+   FnBody.ret `x;
 IO.println $ format fbody
 
 def main : IO Unit :=