diff --git a/src/frontends/lean/lean_parser.cpp b/src/frontends/lean/lean_parser.cpp
index e397641e3..973e683a7 100644
--- a/src/frontends/lean/lean_parser.cpp
+++ b/src/frontends/lean/lean_parser.cpp
@@ -248,14 +248,8 @@ class parser::imp {
 
     /** \brief Initialize \c m_builtins table with Lean builtin symbols that do not have notation associated with them. */
     void init_builtins() {
-        m_builtins["Bool"]   = Bool;
-        m_builtins["true"]   = True;
-        m_builtins["false"]  = False;
         m_builtins["\u22A4"] = True;
         m_builtins["\u22A5"] = False;
-        m_builtins["Nat"]    = Nat;
-        m_builtins["Int"]    = Int;
-        m_builtins["Real"]   = Real;
     }
 
     unsigned parse_unsigned(char const * msg) {
@@ -576,6 +570,8 @@ class parser::imp {
                 } else {
                     return mk_constant(obj.get_name());
                 }
+            } if (k == object_kind::Builtin) {
+                return obj.get_value();
             } else {
                 throw parser_error(sstream() << "invalid object reference, object '" << id << "' is not an expression.", p);
             }
diff --git a/src/frontends/lean/lean_pp.cpp b/src/frontends/lean/lean_pp.cpp
index 0a69054c1..4900f9672 100644
--- a/src/frontends/lean/lean_pp.cpp
+++ b/src/frontends/lean/lean_pp.cpp
@@ -1166,6 +1166,12 @@ class pp_formatter_cell : public formatter_cell {
         return r;
     }
 
+    format pp_builtin_set(object const & obj, options const & opts) {
+        char const * kwd = obj.keyword();
+        name const & n = obj.get_name();
+        return format{highlight_command(format(kwd)), space(), format(n)};
+    }
+
     format pp_definition(object const & obj, options const & opts) {
         return pp_compact_definition(obj.keyword(), obj.get_name(), obj.get_type(), obj.get_value(), opts);
     }
@@ -1224,6 +1230,8 @@ public:
         case object_kind::UVarDeclaration:  return pp_uvar_decl(obj, opts);
         case object_kind::Postulate:        return pp_postulate(obj, opts);
         case object_kind::Definition:       return pp_definition(obj, opts);
+        case object_kind::Builtin:          return pp_postulate(obj, opts);
+        case object_kind::BuiltinSet:       return pp_builtin_set(obj, opts);
         case object_kind::Neutral:
             if (dynamic_cast<notation_declaration const *>(obj.cell())) {
                 return pp_notation_decl(obj, opts);
diff --git a/src/kernel/arith/arith.cpp b/src/kernel/arith/arith.cpp
index ddda46505..7af45633b 100644
--- a/src/kernel/arith/arith.cpp
+++ b/src/kernel/arith/arith.cpp
@@ -353,6 +353,29 @@ void add_arith_theory(environment & env) {
     expr x    = Const("x");
     expr y    = Const("y");
 
+    env.add_builtin(Nat);
+    env.add_builtin_set(nVal(0));
+    env.add_builtin(mk_nat_add_fn());
+    env.add_builtin(mk_nat_mul_fn());
+    env.add_builtin(mk_nat_le_fn());
+
+    env.add_builtin(Int);
+    env.add_builtin_set(iVal(0));
+    env.add_builtin(mk_int_add_fn());
+    env.add_builtin(mk_int_mul_fn());
+    env.add_builtin(mk_int_div_fn());
+    env.add_builtin(mk_int_le_fn());
+
+    env.add_builtin(Real);
+    env.add_builtin_set(rVal(0));
+    env.add_builtin(mk_real_add_fn());
+    env.add_builtin(mk_real_mul_fn());
+    env.add_builtin(mk_real_div_fn());
+    env.add_builtin(mk_real_le_fn());
+
+    env.add_builtin(mk_nat_to_int_fn());
+    env.add_builtin(mk_int_to_real_fn());
+
     env.add_definition(nat_ge_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, nLe(y, x)));
     env.add_definition(nat_lt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(y, x))));
     env.add_definition(nat_gt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(x, y))));
diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp
index c8b6758f3..ee19c4694 100644
--- a/src/kernel/builtin.cpp
+++ b/src/kernel/builtin.cpp
@@ -45,7 +45,6 @@ expr mk_bin_lop(expr const & op, expr const & unit, std::initializer_list<expr>
     return mk_bin_lop(op, unit, l.size(), l.begin());
 }
 
-
 // =======================================
 // Bultin universe variables m and u
 static level m_lvl(name("M"));
@@ -121,19 +120,19 @@ bool is_false(expr const & e) {
 
 // =======================================
 // If-then-else builtin operator
-static name   g_ite_name("ite");
-static format g_ite_fmt(g_ite_name);
-class ite_fn_value : public value {
+static name   g_if_name("if");
+static format g_if_fmt(g_if_name);
+class if_fn_value : public value {
     expr m_type;
 public:
-    ite_fn_value() {
+    if_fn_value() {
         expr A    = Const("A");
         // Pi (A: Type), bool -> A -> A -> A
         m_type = Pi({A, TypeU}, Bool >> (A >> (A >> A)));
     }
-    virtual ~ite_fn_value() {}
+    virtual ~if_fn_value() {}
     virtual expr get_type() const { return m_type; }
-    virtual name get_name() const { return g_ite_name; }
+    virtual name get_name() const { return g_if_name; }
     virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
         if (num_args == 5 && is_bool_value(args[2])) {
             if (to_bool(args[2]))
@@ -149,10 +148,9 @@ public:
         }
     }
 };
-MK_BUILTIN(ite_fn, ite_fn_value);
+MK_BUILTIN(if_fn, if_fn_value);
 // =======================================
 
-MK_CONSTANT(if_fn,      name("if"));
 MK_CONSTANT(implies_fn, name("implies"));
 MK_CONSTANT(iff_fn,     name("iff"));
 MK_CONSTANT(and_fn,     name("and"));
@@ -174,6 +172,7 @@ MK_CONSTANT(imp_antisym_fn, name("ImpAntisym"));
 void add_basic_theory(environment & env) {
     env.add_uvar(uvar_name(m_lvl), level() + LEAN_DEFAULT_LEVEL_SEPARATION);
     env.add_uvar(uvar_name(u_lvl), m_lvl + LEAN_DEFAULT_LEVEL_SEPARATION);
+
     expr p1        = Bool >> Bool;
     expr p2        = Bool >> p1;
     expr f         = Const("f");
@@ -191,18 +190,19 @@ void add_basic_theory(environment & env) {
     expr H         = Const("H");
     expr H1        = Const("H1");
     expr H2        = Const("H2");
-    expr ite       = mk_ite_fn();
 
-    // if(A, x, y, z) := ite A x y z
-    env.add_definition(if_fn_name, to_value(ite).get_type(), ite);
+    env.add_builtin(mk_bool_type());
+    env.add_builtin(mk_bool_value(true));
+    env.add_builtin(mk_bool_value(false));
+    env.add_builtin(mk_if_fn());
 
-    // implies(x, y) := ite x y True
+    // implies(x, y) := if x y True
     env.add_definition(implies_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, bIf(x, y, True)));
 
     // iff(x, y) := x = y
     env.add_definition(iff_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Eq(x, y)));
 
-    // not(x) := ite x False True
+    // not(x) := if x False True
     env.add_definition(not_fn_name, p1, Fun({x, Bool}, bIf(x, False, True)));
 
     // or(x, y) := Not(x) => y
diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp
index 416706ac5..156273136 100644
--- a/src/kernel/environment.cpp
+++ b/src/kernel/environment.cpp
@@ -234,6 +234,22 @@ struct environment::imp {
         check_type(n, t, v, env);
     }
 
+    /** \brief Add a new builtin value to this environment */
+    void add_builtin(expr const & n, environment const & env) {
+        if (!is_value(n))
+            throw invalid_builtin_value_declaration(env, n);
+        check_name(to_value(n).get_name(), env);
+        register_named_object(mk_builtin(n));
+    }
+
+    /** \brief Add a new builtin value set to this environment */
+    void add_builtin_set(expr const & r, environment const & env) {
+        if (!is_value(r))
+            throw invalid_builtin_value_declaration(env, r);
+        check_name(to_value(r).get_name(), env);
+        register_named_object(mk_builtin_set(r));
+    }
+
     /** \brief Add new definition. */
     void add_definition(name const & n, expr const & t, expr const & v, bool opaque, environment const & env) {
         check_new_definition(n, t, v, env);
@@ -378,6 +394,14 @@ level environment::get_uvar(name const & n) const {
     return m_imp->get_uvar(n, *this);
 }
 
+void environment::add_builtin(expr const & v) {
+    return m_imp->add_builtin(v, *this);
+}
+
+void environment::add_builtin_set(expr const & r) {
+    return m_imp->add_builtin_set(r, *this);
+}
+
 void environment::add_definition(name const & n, expr const & t, expr const & v, bool opaque) {
     m_imp->add_definition(n, t, v, opaque, *this);
 }
diff --git a/src/kernel/environment.h b/src/kernel/environment.h
index da32085eb..4bc0ec6ea 100644
--- a/src/kernel/environment.h
+++ b/src/kernel/environment.h
@@ -75,6 +75,27 @@ public:
 
     // =======================================
     // Environment Objects
+
+    /**
+        \brief Add builtin value to the environment.
+
+        \pre is_value(v)
+    */
+    void add_builtin(expr const & v);
+
+    /**
+       \brief Add a builtin value set to the environment.
+
+       The set is registered by providing a representative of the set.
+       Each builtin set of values is implemented by a C++ class.
+       The environment will only accept object of the same class of
+       the representative. This functionality is used to support
+       infinite set of builtin values such as the natural numbers.
+
+       \pre is_value(r);
+    */
+    void add_builtin_set(expr const & r);
+
     /**
        \brief Add a new definition n : t := v.
        It throws an exception if v does not have type t.
diff --git a/src/kernel/kernel_exception.h b/src/kernel/kernel_exception.h
index 8fb6e885b..a7c4ad80f 100644
--- a/src/kernel/kernel_exception.h
+++ b/src/kernel/kernel_exception.h
@@ -170,4 +170,27 @@ public:
     expr const & get_value_type() const { return m_value_type; }
     virtual char const * what() const noexcept { return "definition type mismatch"; }
 };
+
+/**
+    \brief Invalid builtin value declaration.
+*/
+class invalid_builtin_value_declaration : public kernel_exception {
+    expr m_expr;
+public:
+    invalid_builtin_value_declaration(environment const & env, expr const & e):kernel_exception(env), m_expr(e) {}
+    virtual ~invalid_builtin_value_declaration() {}
+    virtual char const * what() const noexcept { return "invalid builtin value declaration, expression is not a builtin value"; }
+};
+
+/**
+    \brief Exception used to report that a builtin value is not
+    declared in the environment.
+*/
+class invalid_builtin_value_reference : public kernel_exception {
+    expr m_expr;
+public:
+    invalid_builtin_value_reference(environment const & env, expr const & e):kernel_exception(env), m_expr(e) {}
+    virtual ~invalid_builtin_value_reference() {}
+    virtual char const * what() const noexcept { return "invalid builtin value reference, this kind of builtin value was not declared in the environment"; }
+};
 }
diff --git a/src/kernel/object.cpp b/src/kernel/object.cpp
index 7564b7937..15fee829f 100644
--- a/src/kernel/object.cpp
+++ b/src/kernel/object.cpp
@@ -9,16 +9,6 @@ Author: Leonardo de Moura
 
 namespace lean {
 neutral_object_cell::neutral_object_cell():object_cell(object_kind::Neutral) {}
-neutral_object_cell::~neutral_object_cell() {}
-bool         neutral_object_cell::has_name() const        { return false; }
-name const & neutral_object_cell::get_name() const        { lean_unreachable(); return name::anonymous(); }
-bool         neutral_object_cell::has_cnstr_level() const { return false; }
-level        neutral_object_cell::get_cnstr_level() const { lean_unreachable(); return level(); }
-bool         neutral_object_cell::has_type() const        { return false; }
-expr const & neutral_object_cell::get_type() const        { lean_unreachable(); return expr::null(); }
-bool         neutral_object_cell::is_definition() const   { return false; }
-bool         neutral_object_cell::is_opaque() const       { lean_unreachable(); return false; }
-expr const & neutral_object_cell::get_value() const       { lean_unreachable(); return expr::null(); }
 
 /**
    \brief Named kernel objects.
@@ -31,8 +21,8 @@ public:
     named_object_cell(object_kind k, name const & n):object_cell(k), m_name(n) {}
     virtual ~named_object_cell() {}
 
-    virtual bool has_name() const          { return true; }
-    virtual name const & get_name() const  { return m_name; }
+    virtual bool has_name() const { return true; }
+    virtual name get_name() const { return m_name; }
 };
 
 /**
@@ -45,18 +35,55 @@ public:
         named_object_cell(object_kind::UVarDeclaration, n), m_level(l) {}
     virtual ~uvar_declaration_object_cell() {}
 
-    virtual bool has_cnstr_level() const   { return true; }
-    virtual level get_cnstr_level() const  { return m_level; }
-
-    bool has_type() const          { return false; }
-    expr const & get_type() const  { lean_unreachable(); return expr::null(); }
-    bool is_definition() const     { return false; }
-    bool is_opaque() const         { lean_unreachable(); return false; }
-    expr const & get_value() const { lean_unreachable(); return expr::null(); }
-
+    virtual bool has_cnstr_level() const { return true; }
+    virtual level get_cnstr_level() const { return m_level; }
     virtual char const * keyword() const { return "Universe"; }
 };
 
+/**
+   \brief Base class for Axioms and Variable declarations.
+*/
+class builtin_object_cell : public object_cell {
+    expr m_value;
+public:
+    builtin_object_cell(expr const & v):
+        object_cell(object_kind::Builtin), m_value(v) { lean_assert(is_value(v)); }
+    virtual ~builtin_object_cell() {}
+    virtual bool has_name() const { return true; }
+    virtual name get_name() const { return to_value(m_value).get_name(); }
+    virtual bool has_type() const { return true; }
+    virtual expr get_type() const { return to_value(m_value).get_type(); }
+    virtual bool is_definition() const { return true; }
+    virtual bool is_opaque() const { return false; }
+    virtual expr get_value() const { return m_value; }
+    virtual char const * keyword() const { return "Builtin"; }
+    virtual bool is_builtin() const { return true; }
+};
+
+/**
+   \brief Base class for capturing a set of builtin objects such as
+      a) the natural numbers 0, 1, 2, ...
+      b) the integers 0, -1, 1, -2, 2, ...
+      c) the reals
+      d) ...
+   This object represents an infinite set of declarations.
+   This is just a markup to sign that an environment depends on a
+   particular builtin set of values.
+*/
+class builtin_set_object_cell : public object_cell {
+    // The representative is only used to test if a builtin value
+    // is in the same C++ class of the representative.
+    expr m_representative;
+public:
+    builtin_set_object_cell(expr const & r):object_cell(object_kind::BuiltinSet), m_representative(r) { lean_assert(is_value(r)); }
+    virtual ~builtin_set_object_cell() {}
+    virtual bool has_name() const { return true; }
+    virtual name get_name() const { return to_value(m_representative).get_name(); }
+    virtual bool is_builtin_set() const { return true; }
+    virtual bool in_builtin_set(expr const & v) const { return is_value(v) && typeid(to_value(v)) == typeid(to_value(m_representative)); }
+    virtual char const * keyword() const { return "BuiltinSet"; }
+};
+
 /**
    \brief Named (and typed) kernel objects.
 */
@@ -67,11 +94,8 @@ public:
         named_object_cell(k, n), m_type(t) {}
     virtual ~named_typed_object_cell() {}
 
-    virtual bool has_type() const          { return true; }
-    virtual expr const & get_type() const  { return m_type; }
-
-    virtual bool has_cnstr_level() const   { return false; }
-    virtual level get_cnstr_level() const  { lean_unreachable(); return level(); }
+    virtual bool has_type() const { return true; }
+    virtual expr get_type() const { return m_type; }
 };
 
 /**
@@ -81,10 +105,6 @@ class postulate_object_cell : public named_typed_object_cell {
 public:
     postulate_object_cell(name const & n, expr const & t):
         named_typed_object_cell(object_kind::Postulate, n, t) {}
-
-    bool is_definition() const     { return false; }
-    bool is_opaque() const         { lean_unreachable(); return false; }
-    expr const & get_value() const { lean_unreachable(); return expr::null(); }
 };
 
 /**
@@ -118,9 +138,9 @@ public:
         named_typed_object_cell(object_kind::Definition, n, t), m_value(v), m_opaque(opaque) {}
     virtual ~definition_object_cell() {}
 
-    bool is_definition() const     { return true; }
-    bool is_opaque() const         { return m_opaque; }
-    expr const & get_value() const { return m_value; }
+    virtual bool is_definition() const     { return true; }
+    virtual bool is_opaque() const         { return m_opaque; }
+    virtual expr get_value() const { return m_value; }
     virtual char const * keyword() const { return "Definition"; }
 };
 
@@ -140,6 +160,8 @@ object mk_definition(name const & n, expr const & t, expr const & v, bool opaque
 object mk_theorem(name const & n, expr const & t, expr const & v) { return object(new theorem_object_cell(n, t, v)); }
 object mk_axiom(name const & n, expr const & t) { return object(new axiom_object_cell(n, t)); }
 object mk_var_decl(name const & n, expr const & t) { return object(new variable_decl_object_cell(n, t)); }
+object mk_builtin(expr const & v) { return object(new builtin_object_cell(v)); }
+object mk_builtin_set(expr const & r) { return object(new builtin_set_object_cell(r)); }
 
 static object g_null_object;
 
diff --git a/src/kernel/object.h b/src/kernel/object.h
index 3271fa257..8794ff4a7 100644
--- a/src/kernel/object.h
+++ b/src/kernel/object.h
@@ -14,7 +14,7 @@ Author: Leonardo de Moura
   frontend may need to create new objects for bookkeeping.
 */
 namespace lean {
-enum class object_kind { UVarDeclaration, Definition, Postulate, Neutral };
+enum class object_kind { UVarDeclaration, Definition, Postulate, Builtin, BuiltinSet, Neutral };
 
 class object_cell {
     void dealloc() { delete this; }
@@ -33,30 +33,34 @@ public:
     virtual char const * keyword() const = 0;
 
     /** \brief Return true iff object has a name. */
-    virtual bool has_name() const = 0;
+    virtual bool has_name() const { return false; }
     /** \brief Return object name. \pre has_name() */
-    virtual name const & get_name() const = 0;
+    virtual name get_name() const { lean_unreachable(); return name(); }
 
     /** \brief Has constraint level associated with it (for universal variables). */
-    virtual bool has_cnstr_level() const = 0;
+    virtual bool has_cnstr_level() const { return false; }
     /** \brief Return the constraint level associated with the object. */
-    virtual level get_cnstr_level() const = 0;
+    virtual level get_cnstr_level() const { lean_unreachable(); return level(); }
 
     /** \brief Return true iff object has a type. */
-    virtual bool has_type() const = 0;
+    virtual bool has_type() const { return false; }
     /** \brief Return object type. \pre has_type() */
-    virtual expr const & get_type() const = 0;
+    virtual expr get_type() const { lean_unreachable(); return expr(); }
 
     /** \brief Return true iff object is a definition */
-    virtual bool is_definition() const = 0;
+    virtual bool is_definition() const { return false; }
     /** \brief Return true iff the definition is opaque. \pre is_definition() */
-    virtual bool is_opaque() const = 0;
+    virtual bool is_opaque() const { lean_unreachable(); return false; }
     /** \brief Return object value. \pre is_definition() */
-    virtual expr const & get_value() const = 0;
+    virtual expr get_value() const { lean_unreachable(); return expr(); }
 
     virtual bool is_axiom() const { return false; }
+    virtual bool is_builtin() const { return false; }
+    virtual bool is_builtin_set() const { return false; }
     virtual bool is_theorem() const { return false; }
     virtual bool is_var_decl() const { return false; }
+
+    virtual bool in_builtin_set(expr const & v) const { return false; }
 };
 
 /**
@@ -67,20 +71,6 @@ public:
 class neutral_object_cell : public object_cell {
 public:
     neutral_object_cell();
-    virtual ~neutral_object_cell();
-
-    virtual bool has_name() const;
-    virtual name const & get_name() const;
-
-    virtual bool has_cnstr_level() const;
-    virtual level get_cnstr_level() const;
-
-    virtual bool has_type() const;
-    virtual expr const & get_type() const;
-
-    virtual bool is_definition() const;
-    virtual bool is_opaque() const;
-    virtual expr const & get_value() const;
 };
 
 /**
@@ -115,25 +105,32 @@ public:
     friend object mk_axiom(name const & n, expr const & t);
     friend object mk_var_decl(name const & n, expr const & t);
     friend object mk_neutral(neutral_object_cell * c);
+    friend object mk_builtin(expr const & v);
+    friend object mk_builtin_set(expr const & r);
 
     char const * keyword() const { return m_ptr->keyword(); }
     bool has_name() const { return m_ptr->has_name(); }
-    name const & get_name() const { return m_ptr->get_name(); }
+    name get_name() const { return m_ptr->get_name(); }
     bool has_type() const { return m_ptr->has_type(); }
     bool has_cnstr_level() const { return m_ptr->has_cnstr_level(); }
     level get_cnstr_level() const { return m_ptr->get_cnstr_level(); }
-    expr const & get_type() const { return m_ptr->get_type(); }
+    expr get_type() const { return m_ptr->get_type(); }
     bool is_definition() const { return m_ptr->is_definition(); }
     bool is_opaque() const { return m_ptr->is_opaque(); }
-    expr const & get_value() const { return m_ptr->get_value(); }
+    expr get_value() const { return m_ptr->get_value(); }
 
     bool is_axiom() const { return m_ptr->is_axiom(); }
     bool is_theorem() const { return m_ptr->is_theorem(); }
     bool is_var_decl() const { return m_ptr->is_var_decl(); }
+    bool is_builtin() const { return m_ptr->is_builtin(); }
+    bool is_builtin_set() const { return m_ptr->is_builtin_set(); }
+    bool in_builtin_set(expr const & e) const { return m_ptr->in_builtin_set(e); }
 
     object_cell const * cell() const { return m_ptr; }
 };
 object mk_uvar_decl(name const & n, level const & l);
+object mk_builtin(expr const & v);
+object mk_builtin_set(expr const & r);
 object mk_definition(name const & n, expr const & t, expr const & v, bool opaque);
 object mk_theorem(name const & n, expr const & t, expr const & v);
 object mk_axiom(name const & n, expr const & t);
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index 02718befa..4aa954c8c 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -139,10 +139,18 @@ public:
             }
             break;
         }
-        case expr_kind::Value:
-            r = to_value(e).get_type();
+        case expr_kind::Value: {
+            // Check if the builtin value (or its set) is declared in the environment.
+            name const & n = to_value(e).get_name();
+            object const & obj = m_env.get_object(n);
+            if (obj && ((obj.is_builtin() && obj.get_value() == e) || (obj.is_builtin_set() && obj.in_builtin_set(e)))) {
+                r = to_value(e).get_type();
+            } else {
+                throw invalid_builtin_value_reference(m_env, e);
+            }
             break;
         }
+        }
 
         if (shared) {
             m_cache.insert(e, r);
diff --git a/src/library/printer.cpp b/src/library/printer.cpp
index b5645fead..6cf6352ec 100644
--- a/src/library/printer.cpp
+++ b/src/library/printer.cpp
@@ -184,8 +184,10 @@ std::ostream & operator<<(std::ostream & out, object const & obj) {
         out << obj.get_name() << " >= " << obj.get_cnstr_level(); break;
     case object_kind::Postulate:
         out << obj.get_name() << " : " << obj.get_type(); break;
-    case object_kind::Definition:
+    case object_kind::Definition: case object_kind::Builtin:
         out << obj.get_name() << " : " << obj.get_type() << " :=\n    " << obj.get_value(); break;
+    case object_kind::BuiltinSet:
+        out << obj.get_name(); break;
     case object_kind::Neutral:
         break;
     }
diff --git a/src/tests/frontends/lean/implicit_args.cpp b/src/tests/frontends/lean/implicit_args.cpp
index 3c3943e23..e84fa3488 100644
--- a/src/tests/frontends/lean/implicit_args.cpp
+++ b/src/tests/frontends/lean/implicit_args.cpp
@@ -71,10 +71,10 @@ static void tst1() {
     expr F = Const("F");
     expr g = Const("g");
     expr a = Const("a");
-    expr Nat  = Const("Nat");
-    expr Real = Const("Real");
-    env.add_var("Nat", Type());
-    env.add_var("Real", Type());
+    expr Nat  = Const("N");
+    expr Real = Const("R");
+    env.add_var("N", Type());
+    env.add_var("R", Type());
     env.add_var("F", Pi({{A, Type()}, {B, Type()}, {g, A >> B}}, A));
     env.add_var("f", Nat >> Real);
     expr f = Const("f");
@@ -109,8 +109,8 @@ static void tst2() {
 
 static void tst3() {
     frontend env;
-    expr Nat = Const("Nat");
-    env.add_var("Nat", Type());
+    expr Nat = Const("N");
+    env.add_var("N", Type());
     env.add_var("vec", Nat >> Type());
     expr n   = Const("n");
     expr vec = Const("vec");
@@ -139,8 +139,8 @@ static void tst3() {
 
 static void tst4() {
     frontend env;
-    expr Nat = Const("Nat");
-    env.add_var("Nat", Type());
+    expr Nat = Const("N");
+    env.add_var("N", Type());
     expr R   = Const("R");
     env.add_var("R", Type());
     env.add_var("a", Nat);
@@ -167,8 +167,8 @@ static void tst5() {
     expr b = Const("b");
     expr f = Const("f");
     expr g = Const("g");
-    expr Nat = Const("Nat");
-    env.add_var("Nat", Type());
+    expr Nat = Const("N");
+    env.add_var("N", Type());
     env.add_var("f", Pi({{A,Type()},{a,A},{b,A}}, A));
     env.add_var("g", Nat >> Nat);
     success(Fun({{a,_},{b,_}},g(f(_,a,b))),
diff --git a/src/tests/kernel/arith.cpp b/src/tests/kernel/arith.cpp
index 847af93b1..aff086366 100644
--- a/src/tests/kernel/arith.cpp
+++ b/src/tests/kernel/arith.cpp
@@ -17,7 +17,7 @@ Author: Leonardo de Moura
 using namespace lean;
 
 static void tst1() {
-    environment env;
+    environment env = mk_toplevel();
     expr e = mk_int_value(mpz(10));
     lean_assert(is_int_value(e));
     lean_assert(infer_type(e, env) == Int);
@@ -25,7 +25,7 @@ static void tst1() {
 }
 
 static void tst2() {
-    environment env;
+    environment env = mk_toplevel();
     expr e = iAdd(iVal(10), iVal(30));
     std::cout << e << "\n";
     std::cout << normalize(e, env) << "\n";
@@ -41,7 +41,7 @@ static void tst2() {
 }
 
 static void tst3() {
-    environment env;
+    environment env = mk_toplevel();
     expr e = iMul(iVal(10), iVal(30));
     std::cout << e << "\n";
     std::cout << normalize(e, env) << "\n";
@@ -73,7 +73,7 @@ static void tst4() {
 }
 
 static void tst5() {
-    environment env;
+    environment env = mk_toplevel();
     env.add_var(name("a"), Int);
     expr e = Eq(iVal(3), iVal(4));
     std::cout << e << " --> " << normalize(e, env) << "\n";
diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp
index 7b4c9f2f0..ba597318e 100644
--- a/src/tests/kernel/environment.cpp
+++ b/src/tests/kernel/environment.cpp
@@ -62,7 +62,7 @@ static void tst2() {
 }
 
 static void tst3() {
-    environment env;
+    environment env = mk_toplevel();
     try {
         env.add_definition("a", Int, Const("a"));
         lean_unreachable();
@@ -123,7 +123,7 @@ static void tst4() {
 }
 
 static void tst5() {
-    environment env;
+    environment env = mk_toplevel();
     env.add_definition("a", Int, iVal(1), true); // add opaque definition
     try {
         std::cout << infer_type(iAdd(Const("a"), Int), env) << "\n";
@@ -134,7 +134,7 @@ static void tst5() {
 }
 
 static void tst6() {
-    environment env;
+    environment env = mk_toplevel();
     level u = env.add_uvar("u", level() + 1);
     level w = env.add_uvar("w", u + 1);
     env.add_var("f", mk_arrow(Type(u), Type(u)));
diff --git a/src/tests/kernel/normalizer.cpp b/src/tests/kernel/normalizer.cpp
index 05e1ecc77..787e28d35 100644
--- a/src/tests/kernel/normalizer.cpp
+++ b/src/tests/kernel/normalizer.cpp
@@ -15,6 +15,7 @@ Author: Leonardo de Moura
 #include "expr_sets.h"
 #include "abstract.h"
 #include "kernel_exception.h"
+#include "toplevel.h"
 #include "printer.h"
 using namespace lean;
 
@@ -185,7 +186,7 @@ static void tst2() {
 }
 
 static void tst3() {
-    environment env;
+    environment env = mk_toplevel();
     env.add_var("a", Bool);
     expr t1 = Const("a");
     expr t2 = Const("a");
@@ -212,7 +213,7 @@ static expr mk_big(unsigned depth) {
 static void tst5() {
 #ifndef __APPLE__
     expr t = mk_big(18);
-    environment env;
+    environment env = mk_toplevel();
     env.add_var("f", Bool >> (Bool >> Bool));
     env.add_var("a", Bool);
     normalizer proc(env);
diff --git a/src/tests/kernel/threads.cpp b/src/tests/kernel/threads.cpp
index 038768d86..436d8919b 100644
--- a/src/tests/kernel/threads.cpp
+++ b/src/tests/kernel/threads.cpp
@@ -13,12 +13,13 @@ Author: Leonardo de Moura
 #include "deep_copy.h"
 #include "abstract.h"
 #include "normalizer.h"
+#include "toplevel.h"
 #include "arith.h"
 #include "test.h"
 using namespace lean;
 
 expr normalize(expr const & e) {
-    environment env;
+    environment env = mk_toplevel();
     env.add_var("a", Int);
     env.add_var("b", Int);
     env.add_var("f", Int >> (Int >> Int));
diff --git a/src/tests/kernel/type_checker.cpp b/src/tests/kernel/type_checker.cpp
index 81cac3759..7b9393be9 100644
--- a/src/tests/kernel/type_checker.cpp
+++ b/src/tests/kernel/type_checker.cpp
@@ -73,7 +73,7 @@ static void tst2() {
 }
 
 static void tst3() {
-    environment env;
+    environment env = mk_toplevel();
     expr f = Fun("a", Bool, Eq(Const("a"), True));
     std::cout << infer_type(f, env) << "\n";
     lean_assert(infer_type(f, env) == mk_arrow(Bool, Bool));
@@ -82,7 +82,7 @@ static void tst3() {
 }
 
 static void tst4() {
-    environment env;
+    environment env = mk_toplevel();
     expr a = Eq(iVal(1), iVal(2));
     expr pr   = mk_lambda("x", a, Var(0));
     std::cout << infer_type(pr, env) << "\n";
@@ -218,7 +218,7 @@ static expr mk_big(unsigned depth) {
 static void tst12() {
 #ifndef __APPLE__
     expr t = mk_big(18);
-    environment env;
+    environment env = mk_toplevel();
     env.add_var("f", Int >> (Int >> Int));
     env.add_var("a", Int);
     type_checker checker(env);
diff --git a/tests/lean/arith7.lean.expected.out b/tests/lean/arith7.lean.expected.out
index db3d0aa9e..bc8690699 100644
--- a/tests/lean/arith7.lean.expected.out
+++ b/tests/lean/arith7.lean.expected.out
@@ -6,7 +6,7 @@
 2
 ⊤
   Assumed: y
-ite Int (0 ≤ -3 + y) (-3 + y) (-1 * (-3 + y))
+if Int (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/tst1.lean.expected.out b/tests/lean/tst1.lean.expected.out
index cddeeb831..f0f28b992 100644
--- a/tests/lean/tst1.lean.expected.out
+++ b/tests/lean/tst1.lean.expected.out
@@ -46,4 +46,4 @@ map normal form -->
   f (v1 i H) (v2 i H)
 
 update normal form --> 
-λ (A : Type) (n : N) (v : Π (i : N) (H : i < n), A) (i : N) (d : A) (j : N) (H : j < n), ite A (j = i) d (v j H)
+λ (A : Type) (n : N) (v : Π (i : N) (H : i < n), A) (i : N) (d : A) (j : N) (H : j < n), if A (j = i) d (v j H)
diff --git a/tests/lean/tst10.lean.expected.out b/tests/lean/tst10.lean.expected.out
index 9fd43784a..0de41e847 100644
--- a/tests/lean/tst10.lean.expected.out
+++ b/tests/lean/tst10.lean.expected.out
@@ -15,7 +15,7 @@ a ∨ b
 a ∨ a ∨ b
 a ⇒ b ⇒ a
 Bool
-ite Bool a a ⊤
+if Bool a a ⊤
 a
   Assumed: H1
   Assumed: H2
diff --git a/tests/lean/tst17.lean.expected.out b/tests/lean/tst17.lean.expected.out
index 001782e7f..d7c7552c0 100644
--- a/tests/lean/tst17.lean.expected.out
+++ b/tests/lean/tst17.lean.expected.out
@@ -5,6 +5,6 @@
 ∀ a b : Type, ∃ c : Type, (g a b) = (f c)
 Bool
 (λ a : Type,
-   (λ b : Type, ite Bool ((λ x : Type, ite Bool ((g a b) = (f x)) ⊥ ⊤) = (λ x : Type, ⊤)) ⊥ ⊤) =
+   (λ b : Type, if Bool ((λ x : Type, if Bool ((g a b) = (f x)) ⊥ ⊤) = (λ x : Type, ⊤)) ⊥ ⊤) =
    (λ x : Type, ⊤)) =
 (λ x : Type, ⊤)