diff --git a/src/Lean/Data/KVMap.lean b/src/Lean/Data/KVMap.lean
index 41de26e972..48c39a6092 100644
--- a/src/Lean/Data/KVMap.lean
+++ b/src/Lean/Data/KVMap.lean
@@ -14,7 +14,7 @@ inductive DataValue where
   | ofNat    (v : Nat)
   | ofInt    (v : Int)
   | ofSyntax (v : Syntax)
-  deriving Inhabited, BEq
+  deriving Inhabited, BEq, Repr
 
 @[export lean_data_value_beq]
 def DataValue.beqExp (a b : DataValue) : Bool :=
@@ -58,7 +58,7 @@ instance : Coe Syntax DataValue := ⟨DataValue.ofSyntax⟩
    generate C++ code from Lean code. -/
 structure KVMap where
   entries : List (Name × DataValue) := []
-  deriving Inhabited
+  deriving Inhabited, Repr
 
 namespace KVMap
 instance : ToString KVMap := ⟨fun m => toString m.entries⟩
diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean
index bcf8603a23..96ed993968 100644
--- a/src/Lean/Expr.lean
+++ b/src/Lean/Expr.lean
@@ -79,7 +79,7 @@ abbrev MData.empty : MData := {}
    binderInfo     : 3-bits
    approxDepth    : 8-bits -- the approximate depth is used to minimize the number of hash collisions
    looseBVarRange : 16-bits -/
-def Expr.Data := UInt64
+def Expr.Data := UInt64 deriving Repr
 
 instance: Inhabited Expr.Data :=
   inferInstanceAs (Inhabited UInt64)
@@ -128,9 +128,9 @@ def BinderInfo.toUInt64 : BinderInfo → UInt64
   | BinderInfo.instImplicit   => 3
   | BinderInfo.auxDecl        => 4
 
-@[inline] private def Expr.mkDataCore
-    (h : UInt64) (looseBVarRange : Nat) (approxDepth : UInt8)
-    (hasFVar hasExprMVar hasLevelMVar hasLevelParam nonDepLet : Bool) (bi : BinderInfo)
+def Expr.mkData
+    (h : UInt64) (looseBVarRange : Nat := 0) (approxDepth : UInt8 := 0)
+    (hasFVar hasExprMVar hasLevelMVar hasLevelParam : Bool := false) (bi : BinderInfo := BinderInfo.default) (nonDepLet : Bool := false)
     : Expr.Data :=
   if looseBVarRange > Nat.pow 2 16 - 1 then panic! "bound variable index is too big"
   else
@@ -146,14 +146,11 @@ def BinderInfo.toUInt64 : BinderInfo → UInt64
       looseBVarRange.toUInt64.shiftLeft 48
     r
 
-def Expr.mkData (h : UInt64) (looseBVarRange : Nat := 0) (approxDepth : UInt8 := 0) (hasFVar hasExprMVar hasLevelMVar hasLevelParam : Bool := false) : Expr.Data :=
-  Expr.mkDataCore h looseBVarRange approxDepth hasFVar hasExprMVar hasLevelMVar hasLevelParam false BinderInfo.default
+@[inline] def Expr.mkDataForBinder (h : UInt64) (looseBVarRange : Nat) (approxDepth : UInt8) (hasFVar hasExprMVar hasLevelMVar hasLevelParam : Bool) (bi : BinderInfo) : Expr.Data :=
+  Expr.mkData h looseBVarRange approxDepth hasFVar hasExprMVar hasLevelMVar hasLevelParam bi false
 
-def Expr.mkDataForBinder (h : UInt64) (looseBVarRange : Nat) (approxDepth : UInt8) (hasFVar hasExprMVar hasLevelMVar hasLevelParam : Bool) (bi : BinderInfo) : Expr.Data :=
-  Expr.mkDataCore h looseBVarRange approxDepth hasFVar hasExprMVar hasLevelMVar hasLevelParam false bi
-
-def Expr.mkDataForLet (h : UInt64) (looseBVarRange : Nat) (approxDepth : UInt8) (hasFVar hasExprMVar hasLevelMVar hasLevelParam nonDepLet : Bool) : Expr.Data :=
-  Expr.mkDataCore h looseBVarRange approxDepth hasFVar hasExprMVar hasLevelMVar hasLevelParam nonDepLet BinderInfo.default
+@[inline] def Expr.mkDataForLet (h : UInt64) (looseBVarRange : Nat) (approxDepth : UInt8) (hasFVar hasExprMVar hasLevelMVar hasLevelParam nonDepLet : Bool) : Expr.Data :=
+  Expr.mkData h looseBVarRange approxDepth hasFVar hasExprMVar hasLevelMVar hasLevelParam BinderInfo.default nonDepLet
 
 open Expr
 
@@ -194,7 +191,7 @@ inductive Expr where
   | lit     : Literal → Data → Expr                   -- literals
   | mdata   : MData → Expr → Data → Expr              -- metadata
   | proj    : Name → Nat → Expr → Data → Expr         -- projection
-  deriving Inhabited
+  deriving Inhabited, Repr
 
 namespace Expr
 
diff --git a/src/Lean/Level.lean b/src/Lean/Level.lean
index 9d6490279b..8c13bab2dd 100644
--- a/src/Lean/Level.lean
+++ b/src/Lean/Level.lean
@@ -22,7 +22,7 @@ namespace Lean
    hasMVar   : 1-bit
    hasParam  : 1-bit
    depth     : 24-bits -/
-def Level.Data := UInt64
+def Level.Data := UInt64 deriving Repr
 
 instance : Inhabited Level.Data :=
   inferInstanceAs (Inhabited UInt64)
@@ -52,7 +52,7 @@ open Level
 
 structure MVarId where
   name : Name
-  deriving Inhabited, BEq, Hashable
+  deriving Inhabited, BEq, Hashable, Repr
 
 instance : Repr MVarId where
   reprPrec n p := reprPrec n.name p
@@ -78,7 +78,7 @@ inductive Level where
   | imax   : Level → Level → Data → Level
   | param  : Name → Data → Level
   | mvar   : MVarId → Data → Level
-  deriving Inhabited
+  deriving Inhabited, Repr
 
 namespace Level
 
diff --git a/tests/lean/mvar1.lean b/tests/lean/mvar1.lean
index 40ab61dc72..e7ddfb9003 100644
--- a/tests/lean/mvar1.lean
+++ b/tests/lean/mvar1.lean
@@ -52,7 +52,7 @@ 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] (mkApp f z)]
 #eval check (!t1.hasFVar)
-#eval t1
+#eval toString t1
 
 def mctx1 : MetavarContext := {}
 def mctx2  := mctx1.addExprMVarDecl `m1 `m1 lctx3 #[] natE
@@ -68,34 +68,34 @@ def mctx10 := mctx9.assignExpr `m1 a
 def t2 := lctx5.mkLambda #[α, x, y] $ mkAppN f #[mkAppN m4 #[α, x, y], x]
 
 #eval check (!t2.hasFVar)
-#eval t2
-#eval (mctx6.instantiateMVars t2).1
+#eval toString t2
+#eval toString (mctx6.instantiateMVars t2).1
 #eval check (!(mctx9.instantiateMVars t2).1.hasMVar)
 #eval check (!(mctx9.instantiateMVars t2).1.hasFVar)
-#eval (mctx9.instantiateMVars t2).1
+#eval toString (mctx9.instantiateMVars t2).1
 
 -- t3 is ill-formed since m3's localcontext contains ‵α`, `x` and `y`
 def t3 := lctx5.mkLambda #[α, x, y] $ mkAppN f #[m3, x]
 #eval check (mctx10.instantiateMVars t3).1.hasFVar
-#eval (mctx7.instantiateMVars t3).1
+#eval toString (mctx7.instantiateMVars t3).1
 
 partial def mkDiamond : Nat → Expr
 | 0     => m1
 | (n+1) => mkAppN f #[mkDiamond n, mkDiamond n]
 
-#eval (mctx7.instantiateMVars (mkDiamond 3)).1
-#eval (mctx10.instantiateMVars (mkDiamond 3)).1
-#eval (mctx7.instantiateMVars (mkDiamond 100)).1.getAppFn
-#eval (mctx10.instantiateMVars (mkDiamond 100)).1.getAppFn
+#eval toString (mctx7.instantiateMVars (mkDiamond 3)).1
+#eval toString (mctx10.instantiateMVars (mkDiamond 3)).1
+#eval toString (mctx7.instantiateMVars (mkDiamond 100)).1.getAppFn
+#eval toString (mctx10.instantiateMVars (mkDiamond 100)).1.getAppFn
 
 def mctx11 := mctx10.assignDelayed `m6 lctx5 #[α, x, y] m5
 def mctx12 := mctx11.assignExpr `m5 (arrow α α)
 
 def t4 := lctx6.mkLambda #[α, x, y, w] $ mkAppN f #[mkAppN m4 #[α, x, y], x]
 
-#eval t4
-#eval (mctx9.instantiateMVars t4).1
-#eval (mctx12.instantiateMVars t4).1
+#eval toString t4
+#eval toString (mctx9.instantiateMVars t4).1
+#eval toString (mctx12.instantiateMVars t4).1
 #eval check (mctx9.instantiateMVars t4).1.hasMVar
 #eval check (!((mctx9.instantiateMVars t4).1.hasFVar))
 #eval check (!(mctx12.instantiateMVars t4).1.hasMVar)
diff --git a/tests/lean/mvar1.lean.expected.out b/tests/lean/mvar1.lean.expected.out
index a9c260ec31..9f5faa5ddf 100644
--- a/tests/lean/mvar1.lean.expected.out
+++ b/tests/lean/mvar1.lean.expected.out
@@ -1,20 +1,20 @@
 
-fun (α : Type) (x : Nat) (y : α) => f α (g x y) (fun (z : Vec.{0} x) => f z)
+"fun (α : Type) (x : Nat) (y : α) => f α (g x y) (fun (z : Vec.{0} x) => f z)"
 
-fun (α : Type) (x : Nat) (y : α) => f (?m4 α x y) x
-fun (α : Type) (x : Nat) (y : α) => f (?m4 α x y) x
+"fun (α : Type) (x : Nat) (y : α) => f (?m4 α x y) x"
+"fun (α : Type) (x : Nat) (y : α) => f (?m4 α x y) x"
 
 
-fun (α : Type) (x : Nat) (y : α) => f (g x y) x
+"fun (α : Type) (x : Nat) (y : α) => f (g x y) x"
 
-fun (α : Type) (x : Nat) (y : α) => f ?m3 x
-f (f (f ?m1 ?m1) (f ?m1 ?m1)) (f (f ?m1 ?m1) (f ?m1 ?m1))
-f (f (f a a) (f a a)) (f (f a a) (f a a))
-f
-f
-fun (α : Type) (x : Nat) (y : α) (w : Nat -> (?m6 α x y)) => f (?m4 α x y) x
-fun (α : Type) (x : Nat) (y : α) (w : Nat -> (?m6 α x y)) => f (g x y) x
-fun (α : Type) (x : Nat) (y : α) (w : Nat -> α -> α) => f (g x y) x
+"fun (α : Type) (x : Nat) (y : α) => f ?m3 x"
+"f (f (f ?m1 ?m1) (f ?m1 ?m1)) (f (f ?m1 ?m1) (f ?m1 ?m1))"
+"f (f (f a a) (f a a)) (f (f a a) (f a a))"
+"f"
+"f"
+"fun (α : Type) (x : Nat) (y : α) (w : Nat -> (?m6 α x y)) => f (?m4 α x y) x"
+"fun (α : Type) (x : Nat) (y : α) (w : Nat -> (?m6 α x y)) => f (g x y) x"
+"fun (α : Type) (x : Nat) (y : α) (w : Nat -> α -> α) => f (g x y) x"
 
 
 
diff --git a/tests/lean/mvar2.lean b/tests/lean/mvar2.lean
index 4e4f49545e..ae312a19fa 100644
--- a/tests/lean/mvar2.lean
+++ b/tests/lean/mvar2.lean
@@ -57,6 +57,6 @@ def mctx7  := mctx6.assignExpr `m1 natE
 def t2 := lctx4.mkLambda #[α, x, y] $ mkAppN f #[mkAppN m3 #[α, x], x]
 
 #eval check (!t2.hasFVar)
-#eval t2
-#eval (mctx6.instantiateMVars t2).1
-#eval (mctx7.instantiateMVars t2).1
+#eval toString t2
+#eval toString (mctx6.instantiateMVars t2).1
+#eval toString (mctx7.instantiateMVars t2).1
diff --git a/tests/lean/mvar2.lean.expected.out b/tests/lean/mvar2.lean.expected.out
index df99e8af6f..8d86c66231 100644
--- a/tests/lean/mvar2.lean.expected.out
+++ b/tests/lean/mvar2.lean.expected.out
@@ -1,4 +1,4 @@
 
-fun (α : Type) (x : ?m1) (y : Nat -> (?m3 α x)) => f (?m3 α x) x
-fun (α : Type) (x : ?m1) (y : Nat -> α -> α) => f (α -> α) x
-fun (α : Type) (x : Nat) (y : Nat -> α -> α) => f (α -> α) x
+"fun (α : Type) (x : ?m1) (y : Nat -> (?m3 α x)) => f (?m3 α x) x"
+"fun (α : Type) (x : ?m1) (y : Nat -> α -> α) => f (α -> α) x"
+"fun (α : Type) (x : Nat) (y : Nat -> α -> α) => f (α -> α) x"
diff --git a/tests/lean/mvar3.lean b/tests/lean/mvar3.lean
index 75acd1888f..5e67573ee1 100644
--- a/tests/lean/mvar3.lean
+++ b/tests/lean/mvar3.lean
@@ -76,7 +76,7 @@ def sortNamePairs {α} [Inhabited α] (xs : List (MVarId × α)) : List (MVarId
 
 #eval toString $ sortNames $ mctx5.decls.toList.map (·.1.name)
 #eval toString $ sortNamePairs $ mctx5.eAssignment.toList
-#eval e1
+#eval toString e1
 #eval check (!e1.hasFVar)
 
 def R2 :=
@@ -90,7 +90,7 @@ def mctx6 := R2.1
 #eval toString $ sortNamePairs $ mctx6.eAssignment.toList
 -- ?n.2 was delayed assigned because ?m.3 is synthetic
 #eval toString $ sortNames $ mctx6.dAssignment.toList.map (·.1.name)
-#eval e2
+#eval toString e2
 
 #print "assigning ?m1 and ?n.1"
 def R3 :=
@@ -100,4 +100,4 @@ let mctx := mctx.assignExpr (Name.mkNum `n 1) (mkLambda `_ bi typeE natE);
 (mctx.instantiateMVars e2)
 def e3    := R3.1
 def mctx7 := R3.2
-#eval e3
+#eval toString e3
diff --git a/tests/lean/mvar3.lean.expected.out b/tests/lean/mvar3.lean.expected.out
index 0a143e659b..8d2bde1ffc 100644
--- a/tests/lean/mvar3.lean.expected.out
+++ b/tests/lean/mvar3.lean.expected.out
@@ -1,10 +1,10 @@
 "[n.1, n.2, n.3, m1, m2, m3]"
 "[(m1, ?n α), (m2, ?n α x), (m3, ?n α x)]"
-fun (α : Type) (x : ?n α) (y : Nat -> (?n α x)) => f (?n α x) x
+"fun (α : Type) (x : ?n α) (y : Nat -> (?n α x)) => f (?n α x) x"
 
 "[n.1, n.2, n.3, m1, m2, m3]"
 "[(m1, ?n α), (m2, ?n α x)]"
 "[n.2]"
-fun (α : Type) (x : ?n α) (y : Nat -> (?n α x)) => f (?n α x) y
+"fun (α : Type) (x : ?n α) (y : Nat -> (?n α x)) => f (?n α x) y"
 assigning ?m1 and ?n
-fun (α : Type) (x : Nat) (y : Nat -> (?n α x)) => f x y
+"fun (α : Type) (x : Nat) (y : Nat -> (?n α x)) => f x y"