diff --git a/tests/lean/lvl1.lean b/tests/lean/lvl1.lean
index bd2e7044b1..68449f95fb 100644
--- a/tests/lean/lvl1.lean
+++ b/tests/lean/lvl1.lean
@@ -4,16 +4,16 @@ namespace Lean
 namespace Level
 
 def mkMax (xs : Array Level) : Level :=
-xs.foldlFrom max (xs.get! 0) 1
+xs.foldlFrom mkLevelMax (xs.get! 0) 1
 
-#eval toString $ normalize $ succ $ succ $ mkMax #[zero, param `w, succ (succ (succ (param `z))), one, succ (succ (param `x)), zero, param `x, param `y, param `x, param `z, succ one, param `w, succ (param `x)]
-#eval toString $ normalize $ max zero (param `x)
-#eval toString $ normalize $ max (param `x) zero
-#eval toString $ normalize $ max zero one
-#eval toString $ normalize $ succ (max (param `x) (param `x))
-#eval toString $ normalize $ max (imax (param `x) one) (max (succ (param `x)) (param `x))
-#eval toString $ normalize $ imax (imax (param `x) one) (max (succ (param `x)) (param `x))
-#eval toString $ #[zero, succ (succ (param `z)), one, succ (succ (param `x)), zero, param `x, param `y, param `x, param `z, succ (param `x)].qsort normLt
+#eval toString $ normalize $ mkLevelSucc $ mkLevelSucc $ mkMax #[levelZero, mkLevelParam `w, mkLevelSucc (mkLevelSucc (mkLevelSucc (mkLevelParam `z))), levelOne, mkLevelSucc (mkLevelSucc (mkLevelParam `x)), levelZero, mkLevelParam `x, mkLevelParam `y, mkLevelParam `x, mkLevelParam `z, mkLevelSucc levelOne, mkLevelParam `w, mkLevelSucc (mkLevelParam `x)]
+#eval toString $ normalize $ mkLevelMax levelZero (mkLevelParam `x)
+#eval toString $ normalize $ mkLevelMax (mkLevelParam `x) levelZero
+#eval toString $ normalize $ mkLevelMax levelZero levelOne
+#eval toString $ normalize $ mkLevelSucc (mkLevelMax (mkLevelParam `x) (mkLevelParam `x))
+#eval toString $ normalize $ mkLevelMax (mkLevelIMax (mkLevelParam `x) levelOne) (mkLevelMax (mkLevelSucc (mkLevelParam `x)) (mkLevelParam `x))
+#eval toString $ normalize $ mkLevelIMax (mkLevelIMax (mkLevelParam `x) levelOne) (mkLevelMax (mkLevelSucc (mkLevelParam `x)) (mkLevelParam `x))
+#eval toString $ #[levelZero, mkLevelSucc (mkLevelSucc (mkLevelParam `z)), levelOne, mkLevelSucc (mkLevelSucc (mkLevelParam `x)), levelZero, mkLevelParam `x, mkLevelParam `y, mkLevelParam `x, mkLevelParam `z, mkLevelSucc (mkLevelParam `x)].qsort normLt
 
 end Level
 end Lean
diff --git a/tests/lean/mvar1.lean b/tests/lean/mvar1.lean
index 4a8336017b..f480b5be03 100644
--- a/tests/lean/mvar1.lean
+++ b/tests/lean/mvar1.lean
@@ -14,12 +14,12 @@ def b0 := mkBVar 0
 def b1 := mkBVar 1
 def b2 := mkBVar 2
 
-def u := Level.param `u
+def u := mkLevelParam `u
 
-def typeE := mkSort Level.one
+def typeE := mkSort levelOne
 def natE  := mkConst `Nat []
 def boolE := mkConst `Bool []
-def vecE  := mkConst `Vec [Level.zero]
+def vecE  := mkConst `Vec [levelZero]
 
 def α := mkFVar `α
 def x := mkFVar `x
diff --git a/tests/lean/mvar2.lean b/tests/lean/mvar2.lean
index b33e24ee44..72f6d37e4a 100644
--- a/tests/lean/mvar2.lean
+++ b/tests/lean/mvar2.lean
@@ -14,12 +14,12 @@ def b0 := mkBVar 0
 def b1 := mkBVar 1
 def b2 := mkBVar 2
 
-def u := Level.param `u
+def u := mkLevelParam `u
 
-def typeE := mkSort Level.one
+def typeE := mkSort levelOne
 def natE  := mkConst `Nat []
 def boolE := mkConst `Bool []
-def vecE  := mkConst `Vec [Level.zero]
+def vecE  := mkConst `Vec [levelZero]
 
 def α := mkFVar `α
 def x := mkFVar `x
diff --git a/tests/lean/mvar3.lean b/tests/lean/mvar3.lean
index 011d693ee4..87bcfeabb9 100644
--- a/tests/lean/mvar3.lean
+++ b/tests/lean/mvar3.lean
@@ -20,12 +20,12 @@ def b0 := mkBVar 0
 def b1 := mkBVar 1
 def b2 := mkBVar 2
 
-def u := Level.param `u
+def u := mkLevelParam `u
 
-def typeE := mkSort Level.one
+def typeE := mkSort levelOne
 def natE  := mkConst `Nat
 def boolE := mkConst `Bool
-def vecE  := mkConst `Vec [Level.zero]
+def vecE  := mkConst `Vec [levelZero]
 
 def α := mkFVar `α
 def x := mkFVar `x
diff --git a/tests/lean/run/expr1.lean b/tests/lean/run/expr1.lean
index a749904626..159261991c 100644
--- a/tests/lean/run/expr1.lean
+++ b/tests/lean/run/expr1.lean
@@ -16,8 +16,8 @@ do let f   := mkConst `f [];
 #eval tst1
 
 def tst2 : IO Unit :=
-do let l1 := Level.max (Level.param `a) (Level.param `b);
-   let l2 := Level.max (Level.param `b) (Level.param `a);
+do let l1 := mkLevelMax (mkLevelParam `a) (mkLevelParam `b);
+   let l2 := mkLevelMax (mkLevelParam `b) (mkLevelParam `a);
    IO.println l1;
    IO.println l2;
    unless (Level.isEquiv l1 l2) $ throw "not equiv";
@@ -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   := mkLambda `x BinderInfo.default (mkSort Level.zero) (mkAppN f #[a, x0]);
-   let t4   := mkLambda `x BinderInfo.default (mkSort Level.zero) (mkAppN f #[a, x1]);
+   let t3   := mkLambda `x BinderInfo.default (mkSort levelZero) (mkAppN f #[a, x0]);
+   let t4   := mkLambda `x BinderInfo.default (mkSort levelZero) (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";
diff --git a/tests/lean/run/expr_maps.lean b/tests/lean/run/expr_maps.lean
index 409db80501..406c6b418b 100644
--- a/tests/lean/run/expr_maps.lean
+++ b/tests/lean/run/expr_maps.lean
@@ -1,7 +1,7 @@
 import Init.Lean.Expr
 open Lean
 
-def exprType : Expr := mkSort Level.one
+def exprType : Expr := mkSort levelOne
 def biDef           := BinderInfo.default
 def exprNat         := mkConst `Nat []
 -- Type -> Type
diff --git a/tests/lean/run/instuniv.lean b/tests/lean/run/instuniv.lean
index 65c3bc3d83..02ea2f0428 100644
--- a/tests/lean/run/instuniv.lean
+++ b/tests/lean/run/instuniv.lean
@@ -5,8 +5,8 @@ def tst : IO Unit :=
 do env ← importModules [`Init.Data.Array.Default];
    match env.find `Array.foldl with
    | some info => do
-     IO.println (info.instantiateTypeLevelParams [Level.zero, Level.zero]);
-     IO.println (info.instantiateValueLevelParams [Level.zero, Level.zero]);
+     IO.println (info.instantiateTypeLevelParams [levelZero, levelZero]);
+     IO.println (info.instantiateValueLevelParams [levelZero, levelZero]);
      pure ()
    | none      => IO.println ("Array.foldl not found");
    pure ()
diff --git a/tests/lean/run/level.lean b/tests/lean/run/level.lean
index d6565c794f..30a7f8d9a9 100644
--- a/tests/lean/run/level.lean
+++ b/tests/lean/run/level.lean
@@ -1,7 +1,7 @@
 import Init.Lean.Level
 open Lean
 
-#eval Level.zero == Level.zero
-#eval Level.zero == Level.succ Level.zero
-#eval Level.max (Level.succ Level.zero) Level.zero == Level.succ Level.zero
-#eval Level.max (Level.succ Level.zero) Level.zero == Level.max (Level.succ Level.zero) Level.zero
+#eval levelZero == levelZero
+#eval levelZero == mkLevelSucc levelZero
+#eval mkLevelMax (mkLevelSucc levelZero) levelZero == mkLevelSucc levelZero
+#eval mkLevelMax (mkLevelSucc levelZero) levelZero == mkLevelMax (mkLevelSucc levelZero) levelZero
diff --git a/tests/lean/run/meta1.lean b/tests/lean/run/meta1.lean
index d48487bb16..ed2bd438ca 100644
--- a/tests/lean/run/meta1.lean
+++ b/tests/lean/run/meta1.lean
@@ -21,7 +21,7 @@ do env ← importModules mods;
    | EStateM.Result.error err _ => throw (IO.userError (toString err))
 
 def t1 : Expr :=
-let map  := mkConst `List.map [Level.one, Level.one];
+let map  := mkConst `List.map [levelOne, levelOne];
 let nat  := mkConst `Nat [];
 let bool := mkConst `Bool [];
 mkAppN map #[nat, bool]
@@ -29,7 +29,7 @@ mkAppN map #[nat, bool]
 #eval tstInferType [`Init.Data.List] t1
 
 def t2 : Expr :=
-let prop := mkSort Level.zero;
+let prop := mkSort levelZero;
 mkForall `x BinderInfo.default prop prop
 
 #eval tstInferType [`Init.Core] t2
@@ -61,12 +61,12 @@ set_option pp.all true
 #check @List.cons Nat
 
 def t6 : Expr :=
-let map  := mkConst `List.map [Level.one, Level.one];
+let map  := mkConst `List.map [levelOne, levelOne];
 let nat  := mkConst `Nat [];
 let add  := mkConst `Nat.add [];
 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 cons := mkApp (mkConst `List.cons [levelZero]) nat;
+let nil  := mkApp (mkConst `List.nil [levelZero]) nat;
 let one  := mkLit (Literal.natVal 1);
 let four := mkLit (Literal.natVal 4);
 let xs   := mkApp (mkApp cons one) (mkApp (mkApp cons four) nil);
@@ -75,9 +75,9 @@ mkAppN map #[nat, nat, f, xs]
 #eval tstInferType [`Init.Data.List] t6
 #eval tstWHNF [`Init.Data.List] t6
 
-#eval tstInferType [] $ mkSort Level.zero
+#eval tstInferType [] $ mkSort levelZero
 
-#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)))
+#eval tstInferType [`Init.Data.List] $ mkLambda `a BinderInfo.implicit (mkSort levelOne) (mkLambda `x BinderInfo.default (mkBVar 0) (mkLambda `xs BinderInfo.default (mkApp (mkConst `List [levelZero]) (mkBVar 1)) (mkBVar 0)))
 
 def t7 : Expr :=
 let nat  := mkConst `Nat [];
@@ -98,7 +98,7 @@ mkLet `x nat one (mkAppN add #[one, mkBVar 0])
 
 def t9 : Expr :=
 let nat  := mkConst `Nat [];
-mkLet `a (mkSort Level.one) nat (mkForall `x BinderInfo.default (mkBVar 0) (mkBVar 1))
+mkLet `a (mkSort levelOne) nat (mkForall `x BinderInfo.default (mkBVar 0) (mkBVar 1))
 
 #eval tstInferType [`Init.Core] $ t9
 #eval tstWHNF [`Init.Core] $ t9
@@ -114,7 +114,7 @@ mkLet `a (mkSort Level.one) nat (mkForall `x BinderInfo.default (mkBVar 0) (mkBV
 
 def t10 : Expr :=
 let nat  := mkConst `Nat [];
-let refl := mkApp (mkConst `Eq.refl [Level.one]) nat;
+let refl := mkApp (mkConst `Eq.refl [levelOne]) nat;
 mkLambda `a BinderInfo.default nat (mkApp refl (mkBVar 0))
 
 #eval tstInferType [`Init.Core] t10
@@ -125,17 +125,17 @@ mkLambda `a BinderInfo.default nat (mkApp refl (mkBVar 0))
 #eval tstIsProp [`Init.Core] (mkConst `And [])
 
 -- Example where isPropQuick fails
-#eval tstIsProp [`Init.Core] (mkAppN (mkConst `id [Level.zero]) #[mkSort Level.zero, mkAppN (mkConst `And []) #[mkConst `True [], mkConst
+#eval tstIsProp [`Init.Core] (mkAppN (mkConst `id [levelZero]) #[mkSort levelZero, mkAppN (mkConst `And []) #[mkConst `True [], mkConst
  `True []]])
 
-#eval tstIsProp [`Init.Core] (mkAppN (mkConst `Eq [Level.one]) #[mkConst `Nat [], mkLit (Literal.natVal 0), mkLit (Literal.natVal 1)])
+#eval tstIsProp [`Init.Core] (mkAppN (mkConst `Eq [levelOne]) #[mkConst `Nat [], mkLit (Literal.natVal 0), mkLit (Literal.natVal 1)])
 
 #eval tstIsProp [`Init.Core] $
   mkForall `x BinderInfo.default (mkConst `Nat [])
-    (mkAppN (mkConst `Eq [Level.one]) #[mkConst `Nat [], mkBVar 0, mkLit (Literal.natVal 1)])
+    (mkAppN (mkConst `Eq [levelOne]) #[mkConst `Nat [], mkBVar 0, mkLit (Literal.natVal 1)])
 
 #eval tstIsProp [`Init.Core] $
   mkApp
     (mkLambda `x BinderInfo.default (mkConst `Nat [])
-      (mkAppN (mkConst `Eq [Level.one]) #[mkConst `Nat [], mkBVar 0, mkLit (Literal.natVal 1)]))
+      (mkAppN (mkConst `Eq [levelOne]) #[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 dbd7bdc3a4..289591478d 100644
--- a/tests/lean/run/update.lean
+++ b/tests/lean/run/update.lean
@@ -11,11 +11,11 @@ do let f   := mkConst `f [];
    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! [levelOne];
    let x₂  := x.updateConst! [];
-   let s   := mkSort Level.one;
-   let s₁  := s.updateSort! Level.one;
-   let s₂  := s.updateSort! Level.zero;
+   let s   := mkSort levelOne;
+   let s₁  := s.updateSort! levelOne;
+   let s₂  := s.updateSort! levelZero;
    let a   := mkForall `x BinderInfo.default s s;
    let a₁  := a.updateForall! BinderInfo.default s s;
    let a₂  := a.updateForall! BinderInfo.default s₂ s;
diff --git a/tests/lean/typeclass_context.lean b/tests/lean/typeclass_context.lean
index 128359a6ba..5b3aac15b2 100644
--- a/tests/lean/typeclass_context.lean
+++ b/tests/lean/typeclass_context.lean
@@ -42,13 +42,13 @@ get >>= λ (ctx : Context) => pure $ ctx.eInstantiate t₂
 
 def testEUnify6 : EStateM String Context Expr := do
 u ← EStateM.fromStateM Context.uNewMeta;
-let t₁ := mkConst "foo" [Level.zero];
+let t₁ := mkConst "foo" [levelZero];
 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 $ mkSort Level.zero;
+e ← EStateM.fromStateM $ Context.eNewMeta $ mkSort levelZero;
 let t₁ := mkFVar "foo";
 let t₂ := e;
 eUnify t₁ t₂;