diff --git a/src/kernel/arith/arith.cpp b/src/kernel/arith/arith.cpp
index df0063aec..b6700cedc 100644
--- a/src/kernel/arith/arith.cpp
+++ b/src/kernel/arith/arith.cpp
@@ -11,11 +11,19 @@ Author: Leonardo de Moura
 #include "environment.h"
 
 namespace lean {
+class num_type_value : public type_value {
+    name m_unicode;
+public:
+    num_type_value(name const & n, name const & u):type_value(n), m_unicode(u) {}
+    virtual ~num_type_value() {}
+    virtual name get_unicode_name() const { return m_unicode; }
+};
+
 // =======================================
 // Natural numbers
-class nat_type_value : public type_value {
+class nat_type_value : public num_type_value {
 public:
-    nat_type_value():type_value("Nat") {}
+    nat_type_value():num_type_value("Nat", "\u2115") /* ℕ */ {}
 };
 expr const Nat = mk_value(*(new nat_type_value()));
 expr mk_nat_type() { return Nat; }
@@ -99,9 +107,9 @@ MK_CONSTANT(nat_id_fn, name({"Nat", "id"}));
 
 // =======================================
 // Integers
-class int_type_value : public type_value {
+class int_type_value : public num_type_value {
 public:
-    int_type_value():type_value("Int") {}
+    int_type_value():num_type_value("Int", "\u2124") /* ℤ */ {}
 };
 expr const Int = mk_value(*(new int_type_value()));
 expr mk_int_type() { return Int; }
@@ -199,9 +207,9 @@ MK_CONSTANT(int_gt_fn, name({"Int", "gt"}));
 
 // =======================================
 // Reals
-class real_type_value : public type_value {
+class real_type_value : public num_type_value {
 public:
-    real_type_value():type_value("Real") {}
+    real_type_value():num_type_value("Real", "\u211D") /* ℝ */ {}
 };
 expr const Real = mk_value(*(new real_type_value()));
 expr mk_real_type() { return Real; }
diff --git a/tests/lean/arith1.lean.expected.out b/tests/lean/arith1.lean.expected.out
index d2113d250..94e8fde4b 100644
--- a/tests/lean/arith1.lean.expected.out
+++ b/tests/lean/arith1.lean.expected.out
@@ -1,11 +1,11 @@
   Set: pp::colors
   Set: pp::unicode
-Nat
-Nat
-Int
+ℕ
+ℕ
+ℤ
 -10
 5
-Int
+ℤ
   Assumed: x
   Assumed: n
   Assumed: m
diff --git a/tests/lean/arith7.lean.expected.out b/tests/lean/arith7.lean.expected.out
index bc8690699..7f88d3d8d 100644
--- a/tests/lean/arith7.lean.expected.out
+++ b/tests/lean/arith7.lean.expected.out
@@ -6,7 +6,7 @@
 2
 ⊤
   Assumed: y
-if Int (0 ≤ -3 + y) (-3 + y) (-1 * (-3 + y))
+if ℤ (0 ≤ -3 + y) (-3 + y) (-1 * (-3 + y))
 | x + y | > x
   Set: lean::pp::notation
 Int::gt (Int::abs (Int::add x y)) x
diff --git a/tests/lean/implicit1.lean.expected.out b/tests/lean/implicit1.lean.expected.out
index 4d6d60f5b..8238c267e 100644
--- a/tests/lean/implicit1.lean.expected.out
+++ b/tests/lean/implicit1.lean.expected.out
@@ -1,30 +1,30 @@
   Set: pp::colors
   Set: pp::unicode
   Assumed: f
-∀ a : Int, (f a a) > 0
-∀ a b : Int, (f a b) > 0
+∀ a : ℤ, (f a a) > 0
+∀ a b : ℤ, (f a b) > 0
   Assumed: g
-∀ (a : Int) (b : Real), (g a b) > 0
-∀ a b : Int, (g a (f a b)) > 0
+∀ (a : ℤ) (b : ℝ), (g a b) > 0
+∀ a b : ℤ, (g a (f a b)) > 0
   Set: lean::pp::coercion
-∀ a b : Int, (g a (int_to_real (f a b))) > (nat_to_int 0)
-λ a : Nat, a + 1
+∀ a b : ℤ, (g a (int_to_real (f a b))) > (nat_to_int 0)
+λ a : ℕ, a + 1
 Error (line: 10, pos: 18) ambiguous overloads
 Candidates:
-    Real::add : Real → Real → Real
-    Int::add : Int → Int → Int
-    Nat::add : Nat → Nat → Nat
+    Real::add : ℝ → ℝ → ℝ
+    Int::add : ℤ → ℤ → ℤ
+    Nat::add : ℕ → ℕ → ℕ
 Arguments:
     a : lift:0:2 ?M0
     b : lift:0:1 ?M2
-λ a b c : Int, a + c + b
+λ a b c : ℤ, a + c + b
 Error (line: 17, pos: 19) ambiguous overloads
 Candidates:
-    Real::add : Real → Real → Real
-    Int::add : Int → Int → Int
-    Nat::add : Nat → Nat → Nat
+    Real::add : ℝ → ℝ → ℝ
+    Int::add : ℤ → ℤ → ℤ
+    Nat::add : ℕ → ℕ → ℕ
 Arguments:
     a : lift:0:2 ?M0
     b : lift:0:1 ?M2
   Assumed: x
-λ a b : Int, a + x + b
+λ a b : ℤ, a + x + b
diff --git a/tests/lean/overload2.lean.expected.out b/tests/lean/overload2.lean.expected.out
index 1d481a8d9..63a51c6a8 100644
--- a/tests/lean/overload2.lean.expected.out
+++ b/tests/lean/overload2.lean.expected.out
@@ -2,11 +2,11 @@
   Set: pp::unicode
 Error (line: 1, pos: 10) application type mismatch, none of the overloads can be used
 Candidates:
-    Real::add : Real → Real → Real
-    Int::add : Int → Int → Int
-    Nat::add : Nat → Nat → Nat
+    Real::add : ℝ → ℝ → ℝ
+    Int::add : ℤ → ℤ → ℤ
+    Nat::add : ℕ → ℕ → ℕ
 Arguments:
-    1 : Nat
+    1 : ℕ
     ⊤ : Bool
   Assumed: R
   Assumed: T
diff --git a/tests/lean/tst14.lean.expected.out b/tests/lean/tst14.lean.expected.out
index 0c0344298..77d252e3c 100644
--- a/tests/lean/tst14.lean.expected.out
+++ b/tests/lean/tst14.lean.expected.out
@@ -1,7 +1,7 @@
   Set: pp::colors
   Set: pp::unicode
-Int → Int → Int
+ℤ → ℤ → ℤ
   Assumed: f
 f 0
-Int → Int
-Int
+ℤ → ℤ
+ℤ
diff --git a/tests/lean/tst8.lean.expected.out b/tests/lean/tst8.lean.expected.out
index 09a98f224..a715ee10c 100644
--- a/tests/lean/tst8.lean.expected.out
+++ b/tests/lean/tst8.lean.expected.out
@@ -3,5 +3,5 @@
 Π (A : Type) (a : A), A
   Assumed: g
   Defined: f
-f Nat 10
-f Int (- 10)
+f ℕ 10
+f ℤ (- 10)