diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt
index 91b9c164c..00dd495fb 100644
--- a/src/kernel/CMakeLists.txt
+++ b/src/kernel/CMakeLists.txt
@@ -1,4 +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)
+  type_check.cpp context.cpp builtin.cpp basic_thms.cpp toplevel.cpp
+  pp.cpp)
 target_link_libraries(kernel ${EXTRA_LIBS})
diff --git a/src/kernel/arith/arith.cpp b/src/kernel/arith/arith.cpp
index c891d616c..6754c0dc5 100644
--- a/src/kernel/arith/arith.cpp
+++ b/src/kernel/arith/arith.cpp
@@ -127,16 +127,16 @@ public:
             return false;
         }
     }
-    virtual void display(std::ostream & out) const { out << "<="; }
-    virtual format pp() const { return format("<="); }
+    virtual void display(std::ostream & out) const { out << "Le"; }
+    virtual format pp() const { return format("Le"); }
     virtual unsigned hash() const { return 67; }
 };
 char const * int_le_value::g_kind = "<=";
 MK_BUILTIN(int_le_fn, int_le_value);
 
-MK_CONSTANT(int_ge_fn, name(name("int"), "ge"));
-MK_CONSTANT(int_lt_fn, name(name("int"), "lt"));
-MK_CONSTANT(int_gt_fn, name(name("int"), "gt"));
+MK_CONSTANT(int_ge_fn, name(name("int"), "Ge"));
+MK_CONSTANT(int_lt_fn, name(name("int"), "Lt"));
+MK_CONSTANT(int_gt_fn, name(name("int"), "Gt"));
 
 void add_int_theory(environment & env) {
     expr p    = Int >> (Int >> Bool);
diff --git a/src/kernel/basic_thms.cpp b/src/kernel/basic_thms.cpp
index 454ce275f..7179e2dd9 100644
--- a/src/kernel/basic_thms.cpp
+++ b/src/kernel/basic_thms.cpp
@@ -32,7 +32,7 @@ MK_CONSTANT(disj2_fn,           name("Disj2"));
 MK_CONSTANT(disj_cases_fn,      name("DisjCases"));
 MK_CONSTANT(symm_fn,            name("Symm"));
 MK_CONSTANT(trans_fn,           name("Trans"));
-MK_CONSTANT(xtrans_fn,          name("xTrans"));
+MK_CONSTANT(trans_ext_fn,       name("TransExt"));
 MK_CONSTANT(congr1_fn,          name("Congr1"));
 MK_CONSTANT(congr2_fn,          name("Congr2"));
 MK_CONSTANT(congr_fn,           name("Congr"));
@@ -207,8 +207,8 @@ void add_basic_thms(environment & env) {
                     Fun({{A, TypeU}, {a, A}, {b, A}, {c, A}, {H1, Eq(a,b)}, {H2, Eq(b,c)}},
                         Subst(A, Fun({x, A}, Eq(a, x)), b, c, H1, H2)));
 
-    // xTrans: Pi (A: Type u) (B : Type u) (a : A) (b c : B) (H1 : a = b) (H2 : b = c), a = c
-    env.add_theorem(xtrans_fn_name, Pi({{A, TypeU}, {B, TypeU}, {a, A}, {b, B}, {c, B}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, Eq(a, c)),
+    // TransExt: Pi (A: Type u) (B : Type u) (a : A) (b c : B) (H1 : a = b) (H2 : b = c), a = c
+    env.add_theorem(trans_ext_fn_name, Pi({{A, TypeU}, {B, TypeU}, {a, A}, {b, B}, {c, B}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, Eq(a, c)),
                     Fun({{A, TypeU}, {B, TypeU}, {a, A}, {b, B}, {c, B}, {H1, Eq(a, b)}, {H2, Eq(b, c)}},
                         Subst(B, Fun({x, B}, Eq(a, x)), b, c, H1, H2)));
 
@@ -259,8 +259,8 @@ void add_basic_thms(environment & env) {
     // Congr : Pi (A : Type u) (B : A -> Type u) (f g : Pi (x : A) B x) (a b : A) (H1 : f = g) (H2 : a = b), f a = g b
     env.add_theorem(congr_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {a, A}, {b, A}, {H1, Eq(f, g)}, {H2, Eq(a, b)}}, Eq(f(a), g(b))),
                     Fun({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {a, A}, {b, A}, {H1, Eq(f, g)}, {H2, Eq(a, b)}},
-                        xTrans(B(a), B(b), f(a), f(b), g(b),
-                               Congr2(A, B, f, a, b, H2), Congr1(A, B, f, g, b, H1))));
+                        TransExt(B(a), B(b), f(a), f(b), g(b),
+                                 Congr2(A, B, f, a, b, H2), Congr1(A, B, f, g, b, H1))));
 
 
     // ForallElim : Pi (A : Type u) (P : A -> bool) (H : (forall A P)) (a : A), P a
diff --git a/src/kernel/basic_thms.h b/src/kernel/basic_thms.h
index ce31528ee..df67741d1 100644
--- a/src/kernel/basic_thms.h
+++ b/src/kernel/basic_thms.h
@@ -93,9 +93,9 @@ expr mk_trans_fn();
 /** \brief (Theorem) A : Type u, a b c : A, H1 : a = b, H2 : b = c |- Trans(A, a, b, c, H1, H2) : a = c */
 inline expr Trans(expr const & A, expr const & a, expr const & b, expr const & c, expr const & H1, expr const & H2) { return mk_app({mk_trans_fn(), A, a, b, c, H1, H2}); }
 
-expr mk_xtrans_fn();
-/** \brief (Theorem) A : Type u, B : Type u, a : A, b c : B, H1 : a = b, H2 : b = c |- xTrans(A, B, a, b, c, H1, H2) : a = c */
-inline expr xTrans(expr const & A, expr const & B, expr const & a, expr const & b, expr const & c, expr const & H1, expr const & H2) { return mk_app({mk_xtrans_fn(), A, B, a, b, c, H1, H2}); }
+expr mk_trans_ext_fn();
+/** \brief (Theorem) A : Type u, B : Type u, a : A, b c : B, H1 : a = b, H2 : b = c |- TransExt(A, B, a, b, c, H1, H2) : a = c */
+inline expr TransExt(expr const & A, expr const & B, expr const & a, expr const & b, expr const & c, expr const & H1, expr const & H2) { return mk_app({mk_trans_ext_fn(), A, B, a, b, c, H1, H2}); }
 
 expr mk_eqt_elim_fn();
 /** \brief (Theorem) a : Bool, H : a = True |- EqTElim(a, H) : a */
diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp
index 7e8caee10..9fef3d1f3 100644
--- a/src/kernel/builtin.cpp
+++ b/src/kernel/builtin.cpp
@@ -165,7 +165,7 @@ public:
     }
     virtual bool operator==(value const & other) const { return other.kind() == kind(); }
     virtual void display(std::ostream & out) const { out << "=>"; }
-    virtual format pp() const { return format("=>"); }
+    virtual format pp() const { return format("implies"); }
     virtual unsigned hash() const { return 23; }
 };
 char const * implies_fn_value::g_kind = "implies";
diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp
index a8a0fbf1a..8535a5ccc 100644
--- a/src/kernel/environment.cpp
+++ b/src/kernel/environment.cpp
@@ -13,6 +13,7 @@ Author: Leonardo de Moura
 #include "safe_arith.h"
 #include "type_check.h"
 #include "exception.h"
+#include "pp.h"
 #include "debug.h"
 
 namespace lean {
@@ -28,13 +29,17 @@ environment::definition::definition(name const & n, expr const & t, expr const &
 environment::definition::~definition() {
 }
 
-void environment::definition::display_header(std::ostream & out) const {
-    out << "Definition";
+void environment::definition::display(std::ostream & out) const {
+    out << header() << " " << m_name << " : " << m_type << " := " << m_value << "\n";
 }
 
-void environment::definition::display(std::ostream & out) const {
-    display_header(out);
-    out << " " << 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):
@@ -45,9 +50,13 @@ environment::fact::fact(name const & n, expr const & 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 {
-    display_header(out);
-    out << " " << m_name << " : " << m_type << "\n";
+    out << header() << " " << m_name << " : " << m_type << "\n";
 }
 
 /** \brief Implementation of the Lean environment. */
@@ -242,18 +251,18 @@ struct environment::imp {
         }
     }
 
-    void display_objects(std::ostream & out) const {
+    void display_objects(std::ostream & out, environment const & env) const {
         for (object const * obj : m_objects) {
-            obj->display(out);
+            out << obj->pp(env) << "\n";
         }
     }
 
     /** \brief Display universal variable constraints and objects stored in this environment and its parents. */
-    void display(std::ostream & out) const {
+    void display(std::ostream & out, environment const & env) const {
         if (has_parent())
-            m_parent->display(out);
+            m_parent->display(out, env);
         display_uvars(out);
-        display_objects(out);
+        display_objects(out, env);
     }
 
     imp():
@@ -375,10 +384,10 @@ environment::object const * environment::get_object_ptr(name const & n) const {
 }
 
 void environment::display_objects(std::ostream & out) const {
-    m_imp->display_objects(out);
+    m_imp->display_objects(out, *this);
 }
 
 void environment::display(std::ostream & out) const {
-    m_imp->display(out);
+    m_imp->display(out, *this);
 }
 }
diff --git a/src/kernel/environment.h b/src/kernel/environment.h
index 54539f0e6..0b95bbe81 100644
--- a/src/kernel/environment.h
+++ b/src/kernel/environment.h
@@ -77,6 +77,8 @@ public:
         It is just a place holder at this point.
     */
     class object {
+    protected:
+        virtual char const * header() const = 0;
     public:
         object() {}
         object(object const & o) = delete;
@@ -85,6 +87,7 @@ public:
         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;
     };
 
@@ -93,7 +96,7 @@ public:
         expr m_type;
         expr m_value;
         bool m_opaque;
-        virtual void display_header(std::ostream & out) const;
+        virtual char const * header() const { return "Definition"; }
     public:
         definition(name const & n, expr const & t, expr const & v, bool opaque);
         virtual ~definition();
@@ -103,10 +106,11 @@ public:
         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;
     };
 
     class theorem : public definition {
-        virtual void display_header(std::ostream & out) const { out << "Theorem"; }
+        virtual char const * header() const { return "Theorem"; }
     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; }
@@ -116,24 +120,24 @@ public:
     protected:
         name m_name;
         expr m_type;
-        virtual void display_header(std::ostream & out) const = 0;
     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 {
-        virtual void display_header(std::ostream & out) const { out << "Axiom"; }
+        virtual char const * header() const { return "Axiom"; }
     public:
         axiom(name const & n, expr const & t):fact(n, t) {}
         virtual object_kind kind() const { return object_kind::Axiom; }
     };
 
     class variable : public fact {
-        virtual void display_header(std::ostream & out) const { out << "Var"; }
+        virtual char const * header() const { return "Variable"; }
     public:
         variable(name const & n, expr const & t):fact(n, t) {}
         virtual object_kind kind() const { return object_kind::Var; }
diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index ccf2b7b42..dd5c8b90b 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -236,70 +236,4 @@ expr copy(expr const & a) {
     return expr();
 }
 }
-
-lean::format pp_aux(lean::expr const & a) {
-    using namespace lean;
-    switch (a.kind()) {
-    case expr_kind::Var:
-        return format{format("#"), format(static_cast<int>(var_idx(a)))};
-    case expr_kind::Constant:
-        return format(const_name(a));
-    case expr_kind::Value:
-        return to_value(a).pp();
-    case expr_kind::App:
-    {
-        format r;
-        for (unsigned i = 0; i < num_args(a); i++) {
-            if (i > 0) r += format(" ");
-            r += pp_aux(arg(a, i));
-        }
-        return paren(r);
-    }
-    case expr_kind::Eq:
-        return paren(format{pp_aux(eq_lhs(a)), format("="), pp_aux(eq_rhs(a))});
-    case expr_kind::Let:
-        return paren(format{
-                       highlight(format("let "), format::format_color::PINK), /* Use unicode lambda */
-                       paren(format{
-                               format(let_name(a)),
-                               format(" := "),
-                               pp_aux(let_value(a))}),
-                       format(" in "),
-                       pp_aux(let_body(a))});
-    case expr_kind::Lambda:
-        return paren(format{
-                       highlight(format("\u03BB "), format::format_color::PINK), /* Use unicode lambda */
-                       paren(format{
-                               format(abst_name(a)),
-                               format(" : "),
-                               pp_aux(abst_domain(a))}),
-                       format(" "),
-                       pp_aux(abst_body(a))});
-    case expr_kind::Pi:
-        return paren(format{
-                       highlight(format("\u03A0 "), format::format_color::ORANGE), /* Use unicode lambda */
-                       paren(format{
-                               format(abst_name(a)),
-                               format(" : "),
-                               pp_aux(abst_domain(a))}),
-                       format(" "),
-                       pp_aux(abst_body(a))});
-    case expr_kind::Type:
-    {
-        std::stringstream ss;
-        ss << ty_level(a);
-
-        return paren(format{format("Type "),
-                            format(ss.str())});
-    }
-    }
-    lean_unreachable();
-    return format();
-}
-
 void print(lean::expr const & a) { std::cout << a << "\n"; }
-
-void pp(lean::expr const & a) {
-    lean::format const & f = pp_aux(a);
-    std::cout << f << "\n";
-}
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index 940b9d717..4e6154898 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -246,6 +246,7 @@ inline bool is_app(expr const & e)         { return e.kind() == expr_kind::App;
 inline bool is_eq(expr const & e)          { return e.kind() == expr_kind::Eq; }
 inline bool is_lambda(expr const & e)      { return e.kind() == expr_kind::Lambda; }
 inline bool is_pi(expr const & e)          { return e.kind() == expr_kind::Pi; }
+       bool is_arrow(expr const & e);
 inline bool is_type(expr const & e)        { return e.kind() == expr_kind::Type; }
 inline bool is_let(expr const & e)         { return e.kind() == expr_kind::Let; }
 inline bool is_abstraction(expr const & e) { return is_lambda(e) || is_pi(e); }
@@ -471,5 +472,4 @@ template<typename F> expr update_eq(expr const & e, F f) {
 }
 // =======================================
 }
-void pp(lean::expr const & a);
 void print(lean::expr const & a);
diff --git a/src/kernel/for_each.h b/src/kernel/for_each.h
new file mode 100644
index 000000000..f828fd96c
--- /dev/null
+++ b/src/kernel/for_each.h
@@ -0,0 +1,52 @@
+/*
+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"
+#include "sets.h"
+
+namespace lean {
+template<typename F>
+class for_each_fn {
+    expr_cell_offset_set m_visited;
+    F                    m_f;
+
+    void apply(expr const & e, unsigned offset) {
+        if (is_shared(e)) {
+            expr_cell_offset p(e.raw(), offset);
+            if (m_visited.find(p) != m_visited.end())
+                return;
+            m_visited.insert(p);
+        }
+
+       m_f(e, offset);
+
+        switch (e.kind()) {
+        case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: case expr_kind::Var:
+            return;
+        case expr_kind::App:
+            std::for_each(begin_args(e), end_args(e), [=](expr const & arg){ return apply(arg, offset); });
+            return;
+        case expr_kind::Eq:
+            apply(eq_lhs(e), offset);
+            apply(eq_rhs(e), offset);
+            return;
+        case expr_kind::Lambda:
+        case expr_kind::Pi:
+            apply(abst_domain(e), offset);
+            apply(abst_body(e), offset + 1);
+            return;
+        case expr_kind::Let:
+            apply(let_value(e), offset);
+            apply(let_body(e), offset + 1);
+            return;
+        }
+    }
+public:
+    for_each_fn(F const & f):m_f(f) {}
+    void operator()(expr const & e) { apply(e, 0); }
+};
+}
diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp
index 840704ebb..25057bf16 100644
--- a/src/kernel/level.cpp
+++ b/src/kernel/level.cpp
@@ -52,7 +52,8 @@ void level_cell::dealloc() {
     case level_kind::Max:     static_cast<level_max*>(this)->~level_max(); delete[] reinterpret_cast<char*>(this); break;
     }
 }
-level::level():                           m_ptr(new level_uvar(name("bot"))) { lean_assert(uvar_name(*this) == name("bot")); }
+static name g_bot_name("bot");
+level::level():                           m_ptr(new level_uvar(g_bot_name)) { lean_assert(uvar_name(*this) == name("bot")); }
 level::level(name const & n):             m_ptr(new level_uvar(n)) {}
 level::level(level const & l, unsigned k):m_ptr(new level_lift(l, k)) { lean_assert(is_uvar(l)); }
 level::level(level_cell * ptr):           m_ptr(ptr) { lean_assert(m_ptr->get_rc() == 1); }
@@ -81,6 +82,10 @@ unsigned level::hash() const {
     return 0;
 }
 
+bool level::is_bottom() const {
+    return is_uvar(*this) && uvar_name(*this) == g_bot_name;
+}
+
 level max_core(unsigned sz, level const * ls) {
     char * mem   = new char[sizeof(level_max) + sz*sizeof(level)];
     return to_level(new (mem) level_max(sz, ls));
@@ -187,6 +192,30 @@ std::ostream & operator<<(std::ostream & out, level const & l) {
     return out;
 }
 
+format pp(level const & l, char const * sep) {
+    switch (kind(l)) {
+    case level_kind::UVar:
+        if (l.is_bottom())
+            return format(0);
+        else
+            return format(uvar_name(l).to_string(sep));
+    case level_kind::Lift:
+        if (lift_of(l).is_bottom())
+            return format(lift_offset(l));
+        else
+            return format{pp(lift_of(l), sep), format(" + "), format(lift_offset(l))};
+    case level_kind::Max: {
+        format r = pp(max_level(l, 0), sep);
+        for (unsigned i = 1; i < max_size(l); i++) {
+            r += format(" \u2293 ");
+            r += pp(max_level(l, i), sep);
+        }
+        return r;
+    }}
+    lean_unreachable();
+    return format();
+}
+
 level max(std::initializer_list<level> const & l) {
     if (l.size() == 1)
         return *(l.begin());
diff --git a/src/kernel/level.h b/src/kernel/level.h
index c67577d80..7fe5d2e29 100644
--- a/src/kernel/level.h
+++ b/src/kernel/level.h
@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include <iostream>
 #include "name.h"
+#include "format.h"
 
 namespace lean {
 class environment;
@@ -34,6 +35,8 @@ public:
 
     unsigned hash() const;
 
+    bool is_bottom() const;
+
     friend level_kind    kind       (level const & l);
     friend name const &  uvar_name  (level const & l);
     friend level const & lift_of    (level const & l);
@@ -61,4 +64,6 @@ inline bool is_max (level const & l) { return kind(l) == level_kind::Max;  }
 
 inline level const * max_begin_levels(level const & l) { return &max_level(l, 0); }
 inline level const * max_end_levels(level const & l)   { return max_begin_levels(l) + max_size(l); }
+
+format pp(level const & l, char const * sep = default_name_separator);
 }
diff --git a/src/kernel/pp.cpp b/src/kernel/pp.cpp
new file mode 100644
index 000000000..14c685b24
--- /dev/null
+++ b/src/kernel/pp.cpp
@@ -0,0 +1,211 @@
+/*
+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 "pp.h"
+#include "environment.h"
+#include "scoped_set.h"
+#include "for_each.h"
+#include "instantiate.h"
+
+namespace lean {
+struct pp_fn {
+    environment const *                  m_env;
+
+    pp_fn(environment const * env):m_env(env) {}
+
+    unsigned indent() const { return 2; }
+    char const * sep() const { return default_name_separator; }
+    format pp_keyword(char const * k) { return highlight(format(k), format::format_color::ORANGE); }
+    format pp_type_kwd() { return highlight(format("Type"), format::format_color::PINK); }
+    format pp_eq_kwd() { return highlight(format(" = "), format::format_color::BLUE); }
+    format pp_lambda_kwd() { return pp_keyword("\u03BB "); }
+    format pp_lambda_arrow() { return format(" \u21D2"); }
+    format pp_pi_kwd() { return pp_keyword("\u03A0 "); }
+    format pp_type_arrow() { return format(" \u2192 "); }
+    format pp_colon() { return format(" : "); }
+    format pp_space() { return format(" "); }
+    format pp_lp() { return format("("); }
+    format pp_rp() { return format(")"); }
+
+    bool is_atomic(expr const & e) {
+        switch (e.kind()) {
+        case expr_kind::Var: case expr_kind::Constant: case expr_kind::Value: case expr_kind::Type:
+            return true;
+        case expr_kind::App: case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Eq: case expr_kind::Let:
+            return false;
+        }
+        return false;
+    }
+
+    format pp_var(expr const & e) {
+        unsigned vidx = var_idx(e);
+        return compose(format("#"), format(vidx));
+    }
+
+    format pp_constant(expr const & e) {
+        return format(const_name(e).to_string(sep()));
+    }
+
+    format pp_value(expr const & e) {
+        return to_value(e).pp();
+    }
+
+    format pp_type(expr const & e) {
+        if (e == Type()) {
+            return pp_type_kwd();
+        } else {
+            return format{pp_type_kwd(), pp_space(), ::lean::pp(ty_level(e), sep())};
+        }
+    }
+
+    format pp_child(expr const & c) {
+        if (is_atomic(c))
+            return pp(c);
+        else
+            return format{pp_lp(), pp(c), pp_rp()};
+    }
+
+    format pp_eq(expr const & e) {
+        return format{pp_child(eq_lhs(e)), pp_eq_kwd(), pp_child(eq_rhs(e))};
+    }
+
+    format pp_app(expr const & e) {
+        // TODO: infix operators, implicit arguments
+
+        // Prefix case
+        format r = pp_child(arg(e, 0));
+        for (unsigned i = 1; i < num_args(e); i++) {
+            r += compose(line(), pp_child(arg(e, i)));
+        }
+        return group(nest(indent(), r));
+    }
+
+    format pp_arrow_body(expr const & e) {
+        if (is_atomic(e) || is_arrow(e))
+            return pp(e);
+        else
+            return pp_child(e);
+    }
+
+    struct is_used {};
+
+    /** \brief Return true iff \c n is already used in body */
+    bool used(name const & n, expr const & body) {
+        auto visitor = [&](expr const & e, unsigned offset) -> void {
+            if (is_constant(e)) {
+                if (const_name(e) == n)
+                    throw is_used();
+            }
+        };
+
+        try {
+            for_each_fn<decltype(visitor)> f(visitor);
+            f(body);
+            return false;
+        } catch (is_used) {
+            return true;
+        }
+    }
+
+    format pp_bname(expr const & binder) {
+        return format(abst_name(binder).to_string(sep()));
+    }
+
+    template<typename It>
+    format pp_bnames(It const & begin, It const & end, bool use_line) {
+        auto it = begin;
+        format r = pp_bname(*it);
+        ++it;
+        for (; it != end; ++it) {
+            r += compose(use_line ? line() : pp_space(), pp_bname(*it));
+        }
+        return r;
+    }
+
+    expr collect_nested(expr const & e, expr_kind k, buffer<expr> & r) {
+        if (e.kind() == k) {
+            r.push_back(e);
+            name const & n = abst_name(e);
+            name n1    = n;
+            unsigned i = 1;
+            while (used(n1, abst_body(e))) {
+                n1 = name(n, i);
+                i++;
+            }
+            expr b = instantiate_with_closed(abst_body(e), mk_constant(n1));
+            return collect_nested(b, k, r);
+        } else {
+            return e;
+        }
+    }
+
+    format pp_abstraction(expr const & e) {
+        if (is_arrow(e)) {
+            return format{pp_child(abst_domain(e)), pp_type_arrow(), pp_arrow_body(abst_body(e))};
+        } else {
+            buffer<expr> nested;
+            expr b = collect_nested(e, e.kind(), nested);
+            lean_assert(b.kind() != e.kind());
+            format head     = is_lambda(e) ? pp_lambda_kwd() : pp_pi_kwd();
+            format body_sep = is_lambda(e) ? pp_lambda_arrow() : format(",");
+
+            if (std::all_of(nested.begin(), nested.end(), [&](expr const & a) { return abst_domain(a) == abst_domain(e); })) {
+                // Domain of all binders is the same
+                format names = pp_bnames(nested.begin(), nested.end(), false);
+                return group(nest(indent(), format{head, names, pp_colon(), pp(abst_domain(e)), body_sep, line(), pp(b)}));
+            } else {
+                auto it  = nested.begin();
+                auto end = nested.end();
+                // PP binders in blocks (names ... : type)
+                bool first = true;
+                format bindings;
+                while (it != end) {
+                    auto it2 = it;
+                    ++it2;
+                    while (it2 != end && abst_domain(*it2) == abst_domain(*it)) {
+                        ++it2;
+                    }
+                    format block = group(nest(indent(), format{pp_lp(), pp_bnames(it, it2, true), pp_colon(), pp(abst_domain(*it)), pp_rp()}));
+                    if (first) {
+                        bindings = block;
+                        first = false;
+                    } else {
+                        bindings += compose(line(), block);
+                    }
+                    it = it2;
+                }
+                return group(nest(indent(), format{head, group(bindings), body_sep, line(), pp(b)}));
+            }
+        }
+    }
+
+    format pp_let(expr const & e) {
+        return format("TODO");
+    }
+
+    format pp(expr const & e) {
+        switch (e.kind()) {
+        case expr_kind::Var:        return pp_var(e);
+        case expr_kind::Constant:   return pp_constant(e);
+        case expr_kind::Value:      return pp_value(e);
+        case expr_kind::App:        return pp_app(e);
+        case expr_kind::Lambda:
+        case expr_kind::Pi:         return pp_abstraction(e);
+        case expr_kind::Type:       return pp_type(e);
+        case expr_kind::Eq:         return pp_eq(e);
+        case expr_kind::Let:        return pp_let(e);
+        }
+        lean_unreachable();
+        return format();
+    }
+
+    format operator()(expr const & e) {
+        return pp(e);
+    }
+};
+format pp(expr const & n) { return pp_fn(0)(n); }
+format pp(expr const & n, environment const & env) { return pp_fn(&env)(n); }
+}
diff --git a/src/kernel/pp.h b/src/kernel/pp.h
new file mode 100644
index 000000000..36e495fd0
--- /dev/null
+++ b/src/kernel/pp.h
@@ -0,0 +1,15 @@
+/*
+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"
+#include "format.h"
+
+namespace lean {
+class environment;
+format pp(expr const & n);
+format pp(expr const & n, environment const & env);
+}
diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp
index 7d53421e9..a51a29f12 100644
--- a/src/tests/kernel/expr.cpp
+++ b/src/tests/kernel/expr.cpp
@@ -14,6 +14,8 @@ Author: Leonardo de Moura
 #include "abstract.h"
 #include "instantiate.h"
 #include "deep_copy.h"
+#include "arith.h"
+#include "pp.h"
 using namespace lean;
 
 void tst1() {
@@ -45,11 +47,11 @@ void tst1_pp() {
     f = Var(0);
     expr fa = f(a);
     expr ty = Type();
-    pp(fa(a)); std::cout << "\n";
-    pp(fa(fa, fa)); std::cout << "\n";
-    pp(mk_lambda("x", ty, Var(0))); std::cout << "\n";
-    pp(mk_pi("x", ty, Var(0))); std::cout << "\n";
-    pp(mk_pi("x", ty, mk_lambda("y", ty, Var(0)))); std::cout << "\n";
+    std::cout << pp(fa(a)) << "\n";
+    std::cout << pp(fa(fa, fa)) << "\n";
+    std::cout << pp(mk_lambda("x", ty, Var(0))) << "\n";
+    std::cout << pp(mk_pi("x", ty, Var(0))) << "\n";
+    std::cout << pp(mk_pi("x", ty, mk_lambda("y", ty, Var(0)))) << "\n";
     std::cerr << "=============== PP =====================\n";
 }
 
@@ -212,11 +214,9 @@ void tst5() {
         std::cout << "count(r1): " << count(r1) << "\n";
         std::cout << "count(r2): " << count(r2) << "\n";
         std::cout << "r1 = " << std::endl;
-        pp(r1);
-        std::cout << std::endl;
+        std::cout << pp(r1) << std::endl;
         std::cout << "r2 = " << std::endl;
-        pp(r2);
-        std::cout << std::endl;
+        std::cout << pp(r2) << std::endl;
         lean_assert(r1 == r2);
     }
     {
@@ -279,8 +279,8 @@ void tst8() {
     lean_assert(!closed(r));
     lean_assert(closed(mk_lambda("z", p, r)));
 
-    pp(mk_lambda("y", p, mk_app({mk_lambda("x", p, y), Var(0)}))); std::cout << std::endl;
-    pp(mk_pi("x", p, f(f(f(a))))); std::cout << std::endl;
+    std::cout << pp(mk_lambda("y", p, mk_app({mk_lambda("x", p, y), Var(0)}))) << std::endl;
+    std::cout << pp(mk_pi("x", p, f(f(f(a))))) << std::endl;
 
 }
 
@@ -371,6 +371,12 @@ void tst15() {
     lean_assert(closed(l));
 }
 
+void tst16() {
+    std::cout << pp(Type() >> ((Int >> Int) >> (Int >> Bool))) << "\n";
+    expr x = Const("x"); expr y = Const("y"); expr f = Const("f");
+    std::cout << pp(Fun({{x, Int}, {y, Int}, {x, Bool}, {f, Pi({x,Bool}, x)}}, f(x, f(Eq(y,Var(3)), iVal(10))))) << "\n";
+}
+
 int main() {
     continue_on_violation(true);
     std::cout << "sizeof(expr):      " << sizeof(expr) << "\n";
@@ -392,6 +398,7 @@ int main() {
     tst13();
     tst14();
     tst15();
+    tst16();
     std::cout << "done" << "\n";
     return has_violations() ? 1 : 0;
 }
diff --git a/src/tests/kernel/level.cpp b/src/tests/kernel/level.cpp
index 3e6fe2a06..3539633e8 100644
--- a/src/tests/kernel/level.cpp
+++ b/src/tests/kernel/level.cpp
@@ -12,10 +12,13 @@ using namespace lean;
 
 static void tst1() {
     environment env;
-    level l1 = env.define_uvar("l1", level());
+    level l1 = env.define_uvar(name(name("l1"), "suffix"), level());
     level l2 = env.define_uvar("l2", l1 + 10);
     level l3 = env.define_uvar("l3", max(l2, l1 + 3));
     level l4 = env.define_uvar("l4", max(l1 + 8, max(l2 + 2, l3 + 20)));
+    std::cout << pp(max(l1 + 8, max(l2 + 2, l3 + 20))) << "\n";
+    std::cout << pp(level()) << "\n";
+    std::cout << pp(level()+1) << "\n";
     env.display_uvars(std::cout);
     lean_assert(env.is_ge(l4 + 10, l3 + 30));
     lean_assert(!env.is_ge(l4 + 9, l3 + 30));
diff --git a/src/util/format.h b/src/util/format.h
index f27ab511a..bac73d640 100644
--- a/src/util/format.h
+++ b/src/util/format.h
@@ -10,6 +10,7 @@ Author: Soonho Kong
 #include <algorithm>
 #include <iostream>
 #include <sstream>
+#include "mpz.h"
 
 namespace lean {
 /**
@@ -143,6 +144,7 @@ public:
     explicit format(std::string const & v):m_value(sexpr_text(sexpr(v))) {}
     explicit format(int v):m_value(sexpr_text(sexpr(v))) {}
     explicit format(double v):m_value(sexpr_text(sexpr(v))) {}
+    explicit format(unsigned v):m_value(sexpr_text(sexpr(mpz(v)))) {}
     explicit format(name const & v):m_value(sexpr_text(sexpr(v))) {}
     explicit format(mpz const & v):m_value(sexpr_text(sexpr(v))) {}
     explicit format(mpq const & v):m_value(sexpr_text(sexpr(v))) {}
diff --git a/src/util/name.cpp b/src/util/name.cpp
index eec4e914d..8224a6025 100644
--- a/src/util/name.cpp
+++ b/src/util/name.cpp
@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include <cstring>
 #include <vector>
 #include <algorithm>
+#include <sstream>
 #include "name.h"
 #include "debug.h"
 #include "rc.h"
@@ -247,7 +248,13 @@ size_t name::size(char const * sep) const {
 }
 
 unsigned name::hash() const {
-    return m_ptr->m_hash;
+    return m_ptr ? m_ptr->m_hash : 11;
+}
+
+std::string name::to_string(char const * sep) const {
+    std::ostringstream s;
+    imp::display(s, sep, m_ptr);
+    return s.str();
 }
 
 std::ostream & operator<<(std::ostream & out, name const & n) {
diff --git a/src/util/name.h b/src/util/name.h
index 524e7f4f8..82c7af267 100644
--- a/src/util/name.h
+++ b/src/util/name.h
@@ -9,7 +9,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 
-constexpr char const * default_name_separator = "::";
+constexpr char const * default_name_separator = "\u2055";
 enum class name_kind { ANONYMOUS, STRING, NUMERAL };
 
 /**
@@ -47,6 +47,10 @@ public:
     char const * get_string() const;
     bool is_atomic() const;
     name get_prefix() const;
+    /**
+       \brief Convert this hierarchical name into a string using the given separator to "glue" the different limbs.
+    */
+    std::string to_string(char const * sep = default_name_separator) const;
     /**
        \brief Size of the this name (in characters) when using the given separator.
     */