diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt
index f90a54348..e65a3c6a8 100644
--- a/src/kernel/CMakeLists.txt
+++ b/src/kernel/CMakeLists.txt
@@ -1,5 +1,5 @@
 add_library(kernel expr.cpp max_sharing.cpp free_vars.cpp abstract.cpp
   instantiate.cpp deep_copy.cpp normalize.cpp level.cpp environment.cpp
   type_check.cpp context.cpp builtin.cpp basic_thms.cpp toplevel.cpp
-  pp.cpp)
+  object.cpp pp.cpp)
 target_link_libraries(kernel ${LEAN_LIBS})
diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp
index 30ae0316c..9065ec59c 100644
--- a/src/kernel/environment.cpp
+++ b/src/kernel/environment.cpp
@@ -17,51 +17,10 @@ Author: Leonardo de Moura
 #include "debug.h"
 
 namespace lean {
-constexpr unsigned uninit = std::numeric_limits<int>::max();
-
-environment::definition::definition(name const & n, expr const & t, expr const & v, bool opaque):
-    m_name(n),
-    m_type(t),
-    m_value(v),
-    m_opaque(opaque) {
-}
-
-environment::definition::~definition() {
-}
-
-void environment::definition::display(std::ostream & out) const {
-    out << header() << " " << m_name << " : " << m_type << " := " << m_value << "\n";
-}
-
-format pp_object_kind(char const * n) { return highlight(format(n), format::format_color::BLUE); }
-constexpr unsigned indentation = 2; // TODO: must be option
-
-format environment::definition::pp(environment const & env) const {
-    return nest(indentation,
-                  format{pp_object_kind(header()), format(" "), format(m_name), format(" : "), ::lean::pp(m_type, env), format(" :="),
-                          line(), ::lean::pp(m_value), format(".")});
-}
-
-environment::fact::fact(name const & n, expr const & t):
-    m_name(n),
-    m_type(t) {
-}
-
-environment::fact::~fact() {
-}
-
-format environment::fact::pp(environment const & env) const {
-    return nest(indentation,
-                format{pp_object_kind(header()), format(" "), format(m_name), format(" : "), ::lean::pp(m_type, env), format(".")});
-}
-
-void environment::fact::display(std::ostream & out) const {
-    out << header() << " " << m_name << " : " << m_type << "\n";
-}
-
 /** \brief Implementation of the Lean environment. */
 struct environment::imp {
-    typedef std::unordered_map<name, object *, name_hash, name_eq> object_dictionary;
+    // Remark: only named objects are stored in the dictionary.
+    typedef std::unordered_map<name, named_object *, name_hash, name_eq> object_dictionary;
     typedef std::tuple<level, level, int> constraint;
     // Universe variable management
     std::vector<constraint>              m_constraints;
@@ -73,25 +32,33 @@ struct environment::imp {
     std::vector<object*>                 m_objects;
     object_dictionary                    m_object_dictionary;
 
+    /**
+       \brief Return true iff this environment has children.
+
+       \remark If an environment has children than it cannot be
+       updated. That is, it is read-only.
+    */
     bool has_children() const { return m_num_children > 0; }
     void inc_children() { m_num_children++; }
     void dec_children() { m_num_children--; }
 
+    /** \brief Return true iff this environment has a parent environment */
     bool has_parent() const { return m_parent != nullptr; }
 
-    /** \brief Return true if l1 >= l2 + k is implied by constraints
-        \pre is_uvar(l1) && is_uvar(l2)
-     */
-    bool is_implied(level const & l1, level const & l2, int k) {
-        lean_assert(is_uvar(l1) && is_uvar(l2));
-        if (l1 == l2)
+    /**
+        \brief Return true if u >= v + k is implied by constraints
+        \pre is_uvar(u) && is_uvar(v)
+    */
+    bool is_implied(level const & u, level const & v, int k) {
+        lean_assert(is_uvar(u) && is_uvar(v));
+        if (u == v)
             return k <= 0;
         else
             return std::any_of(m_constraints.begin(), m_constraints.end(),
-                               [&](constraint const & c) { return std::get<0>(c) == l1 && std::get<1>(c) == l2 && std::get<2>(c) >= k; });
+                               [&](constraint const & c) { return std::get<0>(c) == u && std::get<1>(c) == v && std::get<2>(c) >= k; });
     }
 
-    /** \brief Return true iff l1 >= l2 + k */
+    /** \brief Return true iff l1 >= l2 + k by asserted universe constraints. */
     bool is_ge(level const & l1, level const & l2, int k) {
         if (l1 == l2)
             return k == 0;
@@ -109,6 +76,7 @@ struct environment::imp {
         return false;
     }
 
+    /** \brief Return true iff l1 >= l2 is implied by asserted universe constraints. */
     bool is_ge(level const & l1, level const & l2) {
         if (has_parent())
             return m_parent->is_ge(l1, l2);
@@ -116,6 +84,7 @@ struct environment::imp {
             return is_ge(l1, l2, 0);
     }
 
+    /** \brief Add a new universe variable */
     level add_var(name const & n) {
         if (std::any_of(m_uvars.begin(), m_uvars.end(), [&](level const & l){ return uvar_name(l) == n; }))
             throw exception("invalid universe variable declaration, it has already been declared");
@@ -124,24 +93,37 @@ struct environment::imp {
         return r;
     }
 
-    void add_constraint(level const & l1, level const & l2, int d) {
-        if (is_implied(l1, l2, d))
+    /**
+        \brief Add basic constraint u >= v + d, and all basic
+        constraints implied by transitivity.
+
+        \pre is_uvar(u) && is_uvar(v)
+    */
+    void add_constraint(level const & u, level const & v, int d) {
+        lean_assert(is_uvar(u) && is_uvar(v));
+        if (is_implied(u, v, d))
             return; // redundant
         buffer<constraint> to_add;
         for (constraint const & c : m_constraints) {
-            if (std::get<0>(c) == l2) {
+            if (std::get<0>(c) == v) {
                 level const & l3 = std::get<1>(c);
-                int l1_l3_d = safe_add(d, std::get<2>(c));
-                if (!is_implied(l1, l3, l1_l3_d))
-                    to_add.push_back(constraint(l1, l3, l1_l3_d));
+                int u_l3_d = safe_add(d, std::get<2>(c));
+                if (!is_implied(u, l3, u_l3_d))
+                    to_add.push_back(constraint(u, l3, u_l3_d));
             }
         }
-        m_constraints.push_back(constraint(l1, l2, d));
+        m_constraints.push_back(constraint(u, v, d));
         for (constraint const & c: to_add) {
             m_constraints.push_back(c);
         }
     }
 
+    /**
+        \brief Add all basic constraints implied by n >= l + k
+
+        A basic constraint is a constraint of the form u >= v + k
+        where u and v are universe variables.
+    */
     void add_constraints(level const & n, level const & l, int k) {
         lean_assert(is_uvar(n));
         switch (kind(l)) {
@@ -152,6 +134,7 @@ struct environment::imp {
         lean_unreachable();
     }
 
+    /** \brief Add a new universe variable with constraint n >= l */
     level add_uvar(name const & n, level const & l) {
         if (has_parent())
             throw exception("invalid universe declaration, universe variables can only be declared in top-level environments");
@@ -162,6 +145,11 @@ struct environment::imp {
         return r;
     }
 
+    /**
+        \brief Return the universe variable with given name. Throw an
+        exception if the environment and its ancestors do not
+        contain a universe variable named \c n.
+    */
     level get_uvar(name const & n) const {
         if (has_parent()) {
             return m_parent->get_uvar(n);
@@ -177,10 +165,14 @@ struct environment::imp {
         }
     }
 
+    /**
+       \brief Initialize the set of universe variables with bottom
+    */
     void init_uvars() {
         m_uvars.push_back(level());
     }
 
+    /** \brief Display universe variable constraints */
     void display_uvars(std::ostream & out) const {
         for (constraint const & c : m_constraints) {
             out << uvar_name(std::get<0>(c)) << " >= " << uvar_name(std::get<1>(c));
@@ -190,12 +182,16 @@ struct environment::imp {
         }
     }
 
+    /** \brief Throw exception if environment has children. */
     void check_no_children() {
         if (has_children())
             throw exception("invalid object declaration, environment has children environments");
     }
 
-    void check_name(name const & n) {
+    /** \brief Throw exception if environment or its ancestors already have an object with the given name. */
+    void check_name_core(name const & n) {
+        if (has_parent())
+            m_parent->check_name_core(n);
         if (m_object_dictionary.find(n) != m_object_dictionary.end()) {
             std::ostringstream s;
             s << "environment already contains an object with name '" << n << "'";
@@ -203,32 +199,84 @@ struct environment::imp {
         }
     }
 
-    void check_add(name const & n) {
+    void check_name(name const & n) {
         check_no_children();
+        check_name_core(n);
+    }
+
+    /**
+        \brief Throw an exception if \c t is not a type or type of \c
+        v is not convertible to \c t.
+
+        \remark env is the smart pointer of imp. We need it because
+        infer_universe and infer_type expect an environment instead of environment::imp.
+    */
+    void check_type(name const & n, expr const & t, expr const & v, environment const & env) {
+        infer_universe(t, env);
+        expr v_t = infer_type(v, env);
+        if (!is_convertible(t, v_t, env)) {
+            std::ostringstream buffer;
+            buffer << "type mismatch when defining '" << n << "'\n"
+                   << "expected type:\n" << t << "\n"
+                   << "given type:\n" << v_t;
+            throw exception(buffer.str());
+        }
+    }
+
+    /** \brief Throw exception if it is not a valid new definition */
+    void check_new_definition(name const & n, expr const & t, expr const & v, environment const & env) {
         check_name(n);
+        check_type(n, t, v, env);
     }
 
-    void add_definition(name const & n, expr const & t, expr const & v, bool opaque) {
-        m_objects.push_back(new definition(n, t, v, opaque));
-        m_object_dictionary.insert(std::make_pair(n, m_objects.back()));
+    /** \brief Store new named object inside internal data-structures */
+    void register_named_object(named_object * new_obj) {
+        m_objects.push_back(new_obj);
+        m_object_dictionary.insert(std::make_pair(new_obj->get_name(), new_obj));
     }
 
-    void add_theorem(name const & n, expr const & t, expr const & v) {
-        m_objects.push_back(new theorem(n, t, v));
-        m_object_dictionary.insert(std::make_pair(n, m_objects.back()));
+    /** \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);
+        register_named_object(new definition(n, t, v, opaque));
     }
 
-    void add_axiom(name const & n, expr const & t) {
-        m_objects.push_back(new axiom(n, t));
-        m_object_dictionary.insert(std::make_pair(n, m_objects.back()));
+    /**
+        \brief Add new definition.
+        The type of the new definition is the type of \c v.
+    */
+    void add_definition(name const & n, expr const & v, bool opaque, environment const & env) {
+        check_name(n);
+        expr v_t = infer_type(v, env);
+        register_named_object(new definition(n, v_t, v, opaque));
     }
 
-    void add_var(name const & n, expr const & t) {
-        m_objects.push_back(new variable(n, t));
-        m_object_dictionary.insert(std::make_pair(n, m_objects.back()));
+    /** \brief Add new theorem. */
+    void add_theorem(name const & n, expr const & t, expr const & v, environment const & env) {
+        check_new_definition(n, t, v, env);
+        register_named_object(new theorem(n, t, v));
     }
 
-    object const * get_object_ptr(name const & n) const {
+    /** \brief Add new axiom. */
+    void add_axiom(name const & n, expr const & t, environment const & env) {
+        check_name(n);
+        infer_universe(t, env);
+        register_named_object(new axiom(n, t));
+    }
+
+    /** \brief Add new variable. */
+    void add_var(name const & n, expr const & t, environment const & env) {
+        check_name(n);
+        infer_universe(t, env);
+        register_named_object(new variable(n, t));
+    }
+
+    /**
+        \brief Return the object named \c n in the environment or its
+        ancestors. Return nullptr if there is not object with the
+        given name.
+    */
+    named_object const * get_object_ptr(name const & n) const {
         auto it = m_object_dictionary.find(n);
         if (it == m_object_dictionary.end()) {
             if (has_parent())
@@ -240,8 +288,8 @@ struct environment::imp {
         }
     }
 
-    object const & get_object(name const & n) const {
-        object const * ptr = get_object_ptr(n);
+    named_object const & get_object(name const & n) const {
+        named_object const * ptr = get_object_ptr(n);
         if (ptr) {
             return *ptr;
         } else {
@@ -331,55 +379,31 @@ level environment::get_uvar(name const & n) const {
     return m_imp->get_uvar(n);
 }
 
-void environment::check_type(name const & n, expr const & t, expr const & v) {
-    infer_universe(t, *this);
-    expr v_t = infer_type(v, *this);
-    if (!is_convertible(t, v_t, *this)) {
-        std::ostringstream buffer;
-        buffer << "type mismatch when defining '" << n << "'\n"
-               << "expected type:\n" << t << "\n"
-               << "given type:\n" << v_t;
-        throw exception(buffer.str());
-    }
-}
-
 void environment::add_definition(name const & n, expr const & t, expr const & v, bool opaque) {
-    m_imp->check_no_children();
-    m_imp->check_name(n);
-    check_type(n, t, v);
-    m_imp->add_definition(n, t, v, opaque);
+    m_imp->add_definition(n, t, v, opaque, *this);
 }
 
 void environment::add_theorem(name const & n, expr const & t, expr const & v) {
-    m_imp->check_no_children();
-    m_imp->check_name(n);
-    check_type(n, t, v);
-    m_imp->add_theorem(n, t, v);
+    m_imp->add_theorem(n, t, v, *this);
 }
 
 void environment::add_definition(name const & n, expr const & v, bool opaque) {
-    m_imp->check_add(n);
-    expr v_t = infer_type(v, *this);
-    m_imp->add_definition(n, v_t, v, opaque);
+    m_imp->add_definition(n, v, opaque, *this);
 }
 
 void environment::add_axiom(name const & n, expr const & t) {
-    m_imp->check_add(n);
-    infer_universe(t, *this);
-    m_imp->add_axiom(n, t);
+    m_imp->add_axiom(n, t, *this);
 }
 
 void environment::add_var(name const & n, expr const & t) {
-    m_imp->check_add(n);
-    infer_universe(t, *this);
-    m_imp->add_var(n, t);
+    m_imp->add_var(n, t, *this);
 }
 
-environment::object const & environment::get_object(name const & n) const {
+named_object const & environment::get_object(name const & n) const {
     return m_imp->get_object(n);
 }
 
-environment::object const * environment::get_object_ptr(name const & n) const {
+named_object const * environment::get_object_ptr(name const & n) const {
     return m_imp->get_object_ptr(n);
 }
 
@@ -387,7 +411,7 @@ unsigned environment::get_num_objects() const {
     return m_imp->m_objects.size();
 }
 
-environment::object const & environment::get_object(unsigned i) const {
+object const & environment::get_object(unsigned i) const {
     return *(m_imp->m_objects[i]);
 }
 
diff --git a/src/kernel/environment.h b/src/kernel/environment.h
index 2d91dd059..ed51d9e54 100644
--- a/src/kernel/environment.h
+++ b/src/kernel/environment.h
@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include <iostream>
 #include <memory>
-#include "expr.h"
+#include "object.h"
 #include "level.h"
 
 namespace lean {
@@ -16,8 +16,6 @@ namespace lean {
    datatypes, universe variables, et.c
 */
 class environment {
-public:
-    class object;
 private:
     struct imp;
     std::shared_ptr<imp> m_imp;
@@ -80,86 +78,6 @@ public:
 
     // =======================================
     // Environment Objects
-    enum class object_kind { Definition, Theorem, Var, Axiom };
-    /**
-        \brief Base class for environment objects
-        It is just a place holder at this point.
-    */
-    class object {
-    protected:
-    public:
-        object() {}
-        object(object const & o) = delete;
-        object & operator=(object const & o) = delete;
-
-        virtual ~object() {}
-        virtual object_kind kind() const = 0;
-        virtual void display(std::ostream & out) const = 0;
-        virtual format pp(environment const &) const = 0;
-        virtual expr const & get_type() const = 0;
-        virtual char const * header() const = 0;
-    };
-
-    class definition : public object {
-        name m_name;
-        expr m_type;
-        expr m_value;
-        bool m_opaque;
-    public:
-        definition(name const & n, expr const & t, expr const & v, bool opaque);
-        virtual ~definition();
-        virtual object_kind kind() const { return object_kind::Definition; }
-        name const & get_name()  const { return m_name; }
-        virtual expr const & get_type()  const { return m_type; }
-        expr const & get_value() const { return m_value; }
-        bool         is_opaque() const { return m_opaque; }
-        virtual void display(std::ostream & out) const;
-        virtual format pp(environment const & env) const;
-        virtual char const * header() const { return "Definition"; }
-    };
-
-    class theorem : public definition {
-    public:
-        theorem(name const & n, expr const & t, expr const & v):definition(n, t, v, true) {}
-        virtual object_kind kind() const { return object_kind::Theorem; }
-        virtual char const * header() const { return "Theorem"; }
-    };
-
-    class fact : public object {
-    protected:
-        name m_name;
-        expr m_type;
-    public:
-        fact(name const & n, expr const & t);
-        virtual ~fact();
-        name const & get_name()  const { return m_name; }
-        virtual expr const & get_type()  const { return m_type; }
-        virtual void display(std::ostream & out) const;
-        virtual format pp(environment const &) const;
-    };
-
-    class axiom : public fact {
-    public:
-        axiom(name const & n, expr const & t):fact(n, t) {}
-        virtual object_kind kind() const { return object_kind::Axiom; }
-        virtual char const * header() const { return "Axiom"; }
-    };
-
-    class variable : public fact {
-    public:
-        variable(name const & n, expr const & t):fact(n, t) {}
-        virtual object_kind kind() const { return object_kind::Var; }
-        virtual char const * header() const { return "Variable"; }
-    };
-
-    friend bool is_definition(object const & o) { return o.kind() == object_kind::Definition; }
-    friend bool is_axiom(object const & o) { return o.kind() == object_kind::Axiom; }
-    friend bool is_var(object const & o) { return o.kind() == object_kind::Var; }
-    friend bool is_fact(object const & o) { return is_axiom(o) || is_var(o); }
-
-    friend definition const & to_definition(object const & o) { lean_assert(is_definition(o)); return static_cast<definition const &>(o); }
-    friend fact const & to_fact(object const & o) { lean_assert(is_fact(o)); return static_cast<fact const &>(o); }
-
     /**
        \brief Add a new definition n : t := v.
        It throws an exception if v does not have type t.
@@ -187,13 +105,13 @@ public:
        \brief Return the object with the given name.
        It throws an exception if the environment does not have an object with the given name.
     */
-    object const & get_object(name const & n) const;
+    named_object const & get_object(name const & n) const;
 
     /**
        \brief Return the object with the given name.
        Return nullptr if there is no object with the given name.
     */
-    object const * get_object_ptr(name const & n) const;
+    named_object const * get_object_ptr(name const & n) const;
 
     /** \brief Iterator for Lean environment objects. */
     class object_iterator {
diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index dd5c8b90b..caced6aca 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -19,6 +19,13 @@ unsigned hash_args(unsigned size, expr const * args) {
     return hash(size, [&args](unsigned i){ return args[i].hash(); });
 }
 
+static expr g_null;
+
+expr const & expr::null() {
+    lean_assert(!g_null);
+    return g_null;
+}
+
 expr_cell::expr_cell(expr_kind k, unsigned h):
     m_kind(static_cast<unsigned>(k)),
     m_flags(0),
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index c5293e671..8b33cd1d1 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -79,6 +79,8 @@ public:
     expr(expr && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
     ~expr() { if (m_ptr) m_ptr->dec_ref(); }
 
+    static expr const & null();
+
     friend void swap(expr & a, expr & b) { std::swap(a.m_ptr, b.m_ptr); }
 
     void release() { if (m_ptr) m_ptr->dec_ref(); m_ptr = nullptr; }
@@ -410,6 +412,17 @@ struct args {
 expr copy(expr const & e);
 // =======================================
 
+// =======================================
+// Expression formatter
+class expr_formatter {
+public:
+    virtual ~expr_formatter() {}
+    virtual format operator()(expr const & e) = 0;
+    virtual options const & get_options() const = 0;
+};
+// =======================================
+
+
 // =======================================
 // Update
 template<typename F> expr update_app(expr const & e, F f) {
diff --git a/src/kernel/normalize.cpp b/src/kernel/normalize.cpp
index b1d208123..fdf13d190 100644
--- a/src/kernel/normalize.cpp
+++ b/src/kernel/normalize.cpp
@@ -133,9 +133,9 @@ class normalize_fn {
         case expr_kind::Var:
             return lookup(s, var_idx(a), k);
         case expr_kind::Constant: {
-            environment::object const & obj = m_env.get_object(const_name(a));
-            if (is_definition(obj) && !to_definition(obj).is_opaque()) {
-                return normalize(to_definition(obj).get_value(), value_stack(), 0);
+            named_object const & obj = m_env.get_object(const_name(a));
+            if (obj.is_definition() && !obj.is_opaque()) {
+                return normalize(obj.get_value(), value_stack(), 0);
             }
             else {
                 return svalue(a);
diff --git a/src/kernel/object.cpp b/src/kernel/object.cpp
new file mode 100644
index 000000000..2f31512ac
--- /dev/null
+++ b/src/kernel/object.cpp
@@ -0,0 +1,74 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "object.h"
+#include "environment.h"
+#include "pp.h" // TODO: move to front-end
+
+namespace lean {
+// TODO: delete hardcoded
+format pp_object_kind(char const * n) { return highlight(format(n), format::format_color::BLUE); }
+constexpr unsigned indentation = 2; // TODO: must be option
+//
+
+object::~object() {}
+void object::display(std::ostream & out, environment const & env) const { out << pp(env); }
+
+anonymous_object::~anonymous_object() {}
+bool         anonymous_object::has_name() const      { return false; }
+name const & anonymous_object::get_name() const      { lean_unreachable(); return name::anonymous(); }
+bool         anonymous_object::has_type() const      { return false; }
+expr const & anonymous_object::get_type() const      { lean_unreachable(); return expr::null(); }
+bool         anonymous_object::is_definition() const { return false; }
+bool         anonymous_object::is_opaque() const     { lean_unreachable(); return false; }
+expr const & anonymous_object::get_value() const     { lean_unreachable(); return expr::null(); }
+
+named_object::named_object(name const & n, expr const & t):m_name(n), m_type(t) {}
+named_object::~named_object() {}
+bool         named_object::has_name() const      { return true; }
+name const & named_object::get_name() const      { return m_name; }
+bool         named_object::has_type() const      { return true; }
+expr const & named_object::get_type() const      { return m_type; }
+
+char const * definition::g_keyword = "Definition";
+definition::definition(name const & n, expr const & t, expr const & v, bool opaque):named_object(n, t), m_value(v), m_opaque(opaque) {}
+definition::~definition() {}
+char const * definition::keyword() const       { return g_keyword; }
+bool         definition::is_definition() const { return true; }
+bool         definition::is_opaque() const     { return m_opaque; }
+expr const & definition::get_value() const     { return m_value; }
+format       definition::pp(environment const & env) const {
+    return nest(indentation,
+                format{pp_object_kind(keyword()), format(" "), format(get_name()), format(" : "), ::lean::pp(get_type(), env), format(" :="),
+                        line(), ::lean::pp(get_value()), format(".")});
+}
+
+char const * theorem::g_keyword = "Theorem";
+theorem::theorem(name const & n, expr const & t, expr const & v):definition(n, t, v, true) {}
+theorem::~theorem() {}
+char const * theorem::keyword() const { return g_keyword; }
+
+fact::fact(name const & n, expr const & t):named_object(n, t) {}
+fact::~fact() {}
+bool         fact::is_definition() const { return false; }
+bool         fact::is_opaque() const     { lean_unreachable(); return false; }
+expr const & fact::get_value() const     { lean_unreachable(); return expr::null(); }
+format fact::pp(environment const & env) const {
+    return nest(indentation,
+                format{pp_object_kind(keyword()), format(" "), format(get_name()), format(" : "), ::lean::pp(get_type(), env), format(".")});
+}
+
+char const * axiom::g_keyword = "Axiom";
+axiom::axiom(name const & n, expr const & t):fact(n, t) {}
+axiom::~axiom() {}
+char const * axiom::keyword() const { return g_keyword; }
+
+char const * variable::g_keyword = "Variable";
+variable::variable(name const & n, expr const & t):fact(n, t) {}
+variable::~variable() {}
+char const * variable::keyword() const { return g_keyword; }
+}
+
diff --git a/src/kernel/object.h b/src/kernel/object.h
new file mode 100644
index 000000000..45a0c91b3
--- /dev/null
+++ b/src/kernel/object.h
@@ -0,0 +1,171 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "expr.h"
+
+/*
+  Kernel objects.
+
+  We use abstract classes and virtual methods because a kernel
+  frontend may need to create new objects for bookkeeping.
+*/
+namespace lean {
+class environment;
+
+/**
+   \brief Abstract class used to represent kernel objects (i.e.,
+   definitions, theorems, axioms, recursive definitions, etc)
+*/
+class object {
+protected:
+public:
+    object() {}
+    object(object const & o) = delete;
+    object & operator=(object const & o) = delete;
+    virtual ~object();
+
+    /**
+        \brief Return the keyword used to define this object in a Lean
+        file. The keyword is also used to identify the class of an object.
+    */
+    virtual char const * keyword() const = 0;
+
+    /** \brief Pretty print this object. */
+    virtual format pp(environment const &) const = 0;
+
+    /** \brief Display the object in the standard output. */
+    virtual void display(std::ostream & out, environment const &) const;
+
+    /** \brief Return true iff object has a name. */
+    virtual bool has_name() const = 0;
+
+    /** \brief Return object name. \pre has_name() */
+    virtual name const & get_name() const = 0;
+
+    /** \brief Return true iff object has a type. */
+    virtual bool has_type() const = 0;
+
+    /** \brief Return object type. \pre has_type() */
+    virtual expr const & get_type() const = 0;
+
+    /** \brief Return true iff object is a definition */
+    virtual bool is_definition() const = 0;
+
+    /** \brief Return true iff the definition is opaque. \pre is_definition() */
+    virtual bool is_opaque() const = 0;
+
+    /** \brief Return object value. \pre is_definition() */
+    virtual expr const & get_value() const = 0;
+};
+
+/**
+   \brief Anonymous objects are mainly used for bookkeeping.
+*/
+class anonymous_object : public object {
+public:
+    virtual ~anonymous_object();
+
+    virtual bool has_name() const;
+    virtual name const & get_name() 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;
+};
+
+/**
+   \brief Named (and typed) kernel objects.
+*/
+class named_object : public object {
+    name m_name;
+    expr m_type;
+public:
+    named_object(name const & n, expr const & t);
+    virtual ~named_object();
+
+    virtual bool has_name() const;
+    virtual name const & get_name() const;
+
+    virtual bool has_type() const;
+    virtual expr const & get_type() const;
+};
+
+/**
+   \brief Non-recursive definitions.
+*/
+class definition : public named_object {
+    expr m_value;
+    bool m_opaque; // Opaque definitions are ignored by definitional equality.
+public:
+    definition(name const & n, expr const & t, expr const & v, bool opaque);
+    virtual ~definition();
+
+    static char const * g_keyword;
+    virtual char const * keyword() const;
+
+    virtual bool is_definition() const;
+    virtual bool is_opaque() const;
+    virtual expr const & get_value() const;
+
+    virtual format pp(environment const & env) const;
+};
+
+/**
+   \brief A theorem is essentially an opaque definition.
+*/
+class theorem : public definition {
+public:
+    theorem(name const & n, expr const & t, expr const & v);
+    virtual ~theorem();
+
+    static char const * g_keyword;
+    virtual char const * keyword() const;
+};
+
+/**
+   \brief Base class for named objects that are not definitions.
+*/
+class fact : public named_object {
+public:
+    fact(name const & n, expr const & t);
+    virtual ~fact();
+
+    virtual bool is_definition() const;
+    virtual bool is_opaque() const;
+    virtual expr const & get_value() const;
+
+    virtual format pp(environment const & env) const;
+};
+
+/**
+   \brief Axioms
+*/
+class axiom : public fact {
+public:
+    axiom(name const & n, expr const & t);
+    virtual ~axiom();
+
+    static char const * g_keyword;
+    virtual char const * keyword() const;
+};
+
+/**
+   \brief Variable postulate. It is like an axiom since we are
+   essentially postulating that a type is inhabited.
+*/
+class variable : public fact {
+public:
+    variable(name const & n, expr const & t);
+    virtual ~variable();
+
+    static char const * g_keyword;
+    virtual char const * keyword() const;
+};
+}
diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp
index 5d55f9c0f..297a0e764 100644
--- a/src/tests/kernel/environment.cpp
+++ b/src/tests/kernel/environment.cpp
@@ -68,6 +68,7 @@ static void tst3() {
         std::cout << "expected error: " << ex.what() << "\n";
     }
     env.add_definition("a", Int, iAdd(iVal(1), iVal(2)));
+    std::cout << env << "\n";
     expr t = iAdd(Const("a"), iVal(1));
     std::cout << t << " --> " << normalize(t, env) << "\n";
     lean_assert(normalize(t, env) == iVal(4));
@@ -169,7 +170,7 @@ static void tst7() {
 
 int main() {
     enable_trace("is_convertible");
-    continue_on_violation(true);
+    // continue_on_violation(true);
     tst1();
     tst2();
     tst3();
diff --git a/src/util/name.cpp b/src/util/name.cpp
index 22fa0e8f9..d6315614e 100644
--- a/src/util/name.cpp
+++ b/src/util/name.cpp
@@ -140,6 +140,13 @@ name::~name() {
         m_ptr->dec_ref();
 }
 
+static name g_anonymous;
+
+name const & name::anonymous() {
+    lean_assert(g_anonymous.is_anonymous());
+    return g_anonymous;
+}
+
 name & name::operator=(name const & other) { LEAN_COPY_REF(name, other); }
 
 name & name::operator=(name && other) { LEAN_MOVE_REF(name, other); }
diff --git a/src/util/name.h b/src/util/name.h
index fcb2ba570..fdb5d57d0 100644
--- a/src/util/name.h
+++ b/src/util/name.h
@@ -28,6 +28,7 @@ public:
     name(name && other);
     name(std::initializer_list<char const *> const & l);
     ~name();
+    static name const & anonymous();
     name & operator=(name const & other);
     name & operator=(name && other);
     friend bool operator==(name const & a, name const & b);