diff --git a/src/kernel/arith/arith.cpp b/src/kernel/arith/arith.cpp
index 5796211e1..ddda46505 100644
--- a/src/kernel/arith/arith.cpp
+++ b/src/kernel/arith/arith.cpp
@@ -7,28 +7,15 @@ Author: Leonardo de Moura
 #include "builtin.h"
 #include "arith.h"
 #include "abstract.h"
+#include "value.h"
 #include "environment.h"
 
 namespace lean {
-/** \brief Base class for Nat, Int and Real types */
-class num_type_value : public value {
-    name m_name;
-public:
-    num_type_value(char const * name):m_name(name) {}
-    virtual ~num_type_value() {}
-    virtual expr get_type() const { return Type(); }
-    virtual bool normalize(unsigned num_args, expr const * args, expr & r) const { return false; }
-    virtual void display(std::ostream & out) const { out << m_name; }
-    virtual format pp() const { return format(m_name); }
-    virtual unsigned hash() const { return m_name.hash(); }
-};
-
 // =======================================
 // Natural numbers
-class nat_type_value : public num_type_value {
+class nat_type_value : public type_value {
 public:
-    nat_type_value():num_type_value("Nat") {}
-    virtual bool operator==(value const & other) const { return dynamic_cast<nat_type_value const*>(&other) != nullptr; }
+    nat_type_value():type_value("Nat") {}
 };
 expr const Nat = mk_value(*(new nat_type_value()));
 expr mk_nat_type() { return Nat; }
@@ -39,7 +26,7 @@ public:
     nat_value_value(mpz const & v):m_val(v) { lean_assert(v >= 0); }
     virtual ~nat_value_value() {}
     virtual expr get_type() const { return Nat; }
-    virtual bool normalize(unsigned num_args, expr const * args, expr & r) const { return false; }
+    virtual name get_name() const { return name{"Nat", "numeral"}; }
     virtual bool operator==(value const & other) const {
         nat_value_value const * _other = dynamic_cast<nat_value_value const*>(&other);
         return _other && _other->m_val == m_val;
@@ -64,17 +51,9 @@ mpz const & nat_value_numeral(expr const & e) {
 }
 
 template<char const * Name, typename F>
-class nat_bin_op : public value {
-    expr     m_type;
-    name     m_name;
+class nat_bin_op : public const_value {
 public:
-    nat_bin_op() {
-        m_type = Nat >> (Nat >> Nat);
-        m_name = name("Nat", Name);
-    }
-    virtual ~nat_bin_op() {}
-    virtual expr get_type() const { return m_type; }
-    virtual bool operator==(value const & other) const { return dynamic_cast<nat_bin_op const*>(&other) != nullptr; }
+    nat_bin_op():const_value(name("Nat", Name), Nat >> (Nat >> Nat)) {}
     virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
         if (num_args == 3 && is_nat_value(args[1]) && is_nat_value(args[2])) {
             r = mk_nat_value(F()(nat_value_numeral(args[1]), nat_value_numeral(args[2])));
@@ -83,9 +62,6 @@ public:
             return false;
         }
     }
-    virtual void display(std::ostream & out) const { out << m_name; }
-    virtual format pp() const { return format(m_name); }
-    virtual unsigned hash() const { return m_name.hash(); }
 };
 
 constexpr char nat_add_name[] = "add";
@@ -98,17 +74,9 @@ struct nat_mul_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1
 typedef nat_bin_op<nat_mul_name, nat_mul_eval> nat_mul_value;
 MK_BUILTIN(nat_mul_fn, nat_mul_value);
 
-class nat_le_value : public value {
-    expr m_type;
-    name m_name;
+class nat_le_value : public const_value {
 public:
-    nat_le_value() {
-        m_type = Nat >> (Nat >> Bool);
-        m_name = name{"Nat", "le"};
-    }
-    virtual ~nat_le_value() {}
-    virtual expr get_type() const { return m_type; }
-    virtual bool operator==(value const & other) const { return dynamic_cast<nat_le_value const*>(&other) != nullptr; }
+    nat_le_value():const_value(name{"Nat", "le"}, Nat >> (Nat >> Bool)) {}
     virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
         if (num_args == 3 && is_nat_value(args[1]) && is_nat_value(args[2])) {
             r = mk_bool_value(nat_value_numeral(args[1]) <= nat_value_numeral(args[2]));
@@ -117,9 +85,6 @@ public:
             return false;
         }
     }
-    virtual void display(std::ostream & out) const { out << m_name; }
-    virtual format pp() const { return format(m_name); }
-    virtual unsigned hash() const { return m_name.hash(); }
 };
 MK_BUILTIN(nat_le_fn, nat_le_value);
 
@@ -133,10 +98,9 @@ MK_CONSTANT(nat_id_fn, name({"Nat", "id"}));
 
 // =======================================
 // Integers
-class int_type_value : public num_type_value {
+class int_type_value : public type_value {
 public:
-    int_type_value():num_type_value("Int") {}
-    virtual bool operator==(value const & other) const { return dynamic_cast<int_type_value const*>(&other) != nullptr; }
+    int_type_value():type_value("Int") {}
 };
 expr const Int = mk_value(*(new int_type_value()));
 expr mk_int_type() { return Int; }
@@ -147,7 +111,7 @@ public:
     int_value_value(mpz const & v):m_val(v) {}
     virtual ~int_value_value() {}
     virtual expr get_type() const { return Int; }
-    virtual bool normalize(unsigned num_args, expr const * args, expr & r) const { return false; }
+    virtual name get_name() const { return name{"Int", "numeral"}; }
     virtual bool operator==(value const & other) const {
         int_value_value const * _other = dynamic_cast<int_value_value const*>(&other);
         return _other && _other->m_val == m_val;
@@ -172,17 +136,9 @@ mpz const & int_value_numeral(expr const & e) {
 }
 
 template<char const * Name, typename F>
-class int_bin_op : public value {
-    expr     m_type;
-    name     m_name;
+class int_bin_op : public const_value {
 public:
-    int_bin_op() {
-        m_type = Int >> (Int >> Int);
-        m_name = name("Int", Name);
-    }
-    virtual ~int_bin_op() {}
-    virtual expr get_type() const { return m_type; }
-    virtual bool operator==(value const & other) const { return dynamic_cast<int_bin_op const*>(&other) != nullptr; }
+    int_bin_op():const_value(name("Int", Name), Int >> (Int >> Int)) {}
     virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
         if (num_args == 3 && is_int_value(args[1]) && is_int_value(args[2])) {
             r = mk_int_value(F()(int_value_numeral(args[1]), int_value_numeral(args[2])));
@@ -191,9 +147,6 @@ public:
             return false;
         }
     }
-    virtual void display(std::ostream & out) const { out << m_name; }
-    virtual format pp() const { return format(m_name); }
-    virtual unsigned hash() const { return m_name.hash(); }
 };
 
 constexpr char int_add_name[] = "add";
@@ -218,17 +171,9 @@ struct int_div_eval {
 typedef int_bin_op<int_div_name, int_div_eval> int_div_value;
 MK_BUILTIN(int_div_fn, int_div_value);
 
-class int_le_value : public value {
-    expr m_type;
-    name m_name;
+class int_le_value : public const_value {
 public:
-    int_le_value() {
-        m_type = Int >> (Int >> Bool);
-        m_name = name{"Int", "le"};
-    }
-    virtual ~int_le_value() {}
-    virtual expr get_type() const { return m_type; }
-    virtual bool operator==(value const & other) const { return dynamic_cast<int_le_value const*>(&other) != nullptr; }
+    int_le_value():const_value(name{"Int", "le"}, Int >> (Int >> Bool)) {}
     virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
         if (num_args == 3 && is_int_value(args[1]) && is_int_value(args[2])) {
             r = mk_bool_value(int_value_numeral(args[1]) <= int_value_numeral(args[2]));
@@ -237,9 +182,6 @@ public:
             return false;
         }
     }
-    virtual void display(std::ostream & out) const { out << m_name; }
-    virtual format pp() const { return format(m_name); }
-    virtual unsigned hash() const { return m_name.hash(); }
 };
 MK_BUILTIN(int_le_fn, int_le_value);
 
@@ -255,10 +197,9 @@ MK_CONSTANT(int_gt_fn, name({"Int", "gt"}));
 
 // =======================================
 // Reals
-class real_type_value : public num_type_value {
+class real_type_value : public type_value {
 public:
-    real_type_value():num_type_value("Real") {}
-    virtual bool operator==(value const & other) const { return dynamic_cast<real_type_value const*>(&other) != nullptr; }
+    real_type_value():type_value("Real") {}
 };
 expr const Real = mk_value(*(new real_type_value()));
 expr mk_real_type() { return Real; }
@@ -269,7 +210,7 @@ public:
     real_value_value(mpq const & v):m_val(v) {}
     virtual ~real_value_value() {}
     virtual expr get_type() const { return Real; }
-    virtual bool normalize(unsigned num_args, expr const * args, expr & r) const { return false; }
+    virtual name get_name() const { return name{"Real", "numeral"}; }
     virtual bool operator==(value const & other) const {
         real_value_value const * _other = dynamic_cast<real_value_value const*>(&other);
         return _other && _other->m_val == m_val;
@@ -294,17 +235,9 @@ mpq const & real_value_numeral(expr const & e) {
 }
 
 template<char const * Name, typename F>
-class real_bin_op : public value {
-    expr     m_type;
-    name     m_name;
+class real_bin_op : public const_value {
 public:
-    real_bin_op() {
-        m_type = Real >> (Real >> Real);
-        m_name = name("Real", Name);
-    }
-    virtual ~real_bin_op() {}
-    virtual expr get_type() const { return m_type; }
-    virtual bool operator==(value const & other) const { return dynamic_cast<real_bin_op const*>(&other) != nullptr; }
+    real_bin_op():const_value(name("Real", Name), Real >> (Real >> Real)) {}
     virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
         if (num_args == 3 && is_real_value(args[1]) && is_real_value(args[2])) {
             r = mk_real_value(F()(real_value_numeral(args[1]), real_value_numeral(args[2])));
@@ -313,9 +246,6 @@ public:
             return false;
         }
     }
-    virtual void display(std::ostream & out) const { out << m_name; }
-    virtual format pp() const { return format(m_name); }
-    virtual unsigned hash() const { return m_name.hash(); }
 };
 
 constexpr char real_add_name[] = "add";
@@ -340,17 +270,9 @@ struct real_div_eval {
 typedef real_bin_op<real_div_name, real_div_eval> real_div_value;
 MK_BUILTIN(real_div_fn, real_div_value);
 
-class real_le_value : public value {
-    expr m_type;
-    name m_name;
+class real_le_value : public const_value {
 public:
-    real_le_value() {
-        m_type = Real >> (Real >> Bool);
-        m_name = name{"Real", "le"};
-    }
-    virtual ~real_le_value() {}
-    virtual expr get_type() const { return m_type; }
-    virtual bool operator==(value const & other) const { return dynamic_cast<real_le_value const*>(&other) != nullptr; }
+    real_le_value():const_value(name{"Real", "le"}, Real >> (Real >> Bool)) {}
     virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
         if (num_args == 3 && is_real_value(args[1]) && is_real_value(args[2])) {
             r = mk_bool_value(real_value_numeral(args[1]) <= real_value_numeral(args[2]));
@@ -359,9 +281,6 @@ public:
             return false;
         }
     }
-    virtual void display(std::ostream & out) const { out << m_name; }
-    virtual format pp() const { return format(m_name); }
-    virtual unsigned hash() const { return m_name.hash(); }
 };
 MK_BUILTIN(real_le_fn, real_le_value);
 
@@ -393,17 +312,9 @@ MK_CONSTANT(csch_fn, name("csch"));
 
 // =======================================
 // Coercions
-class nat_to_int_value : public value {
-    expr m_type;
-    name m_name;
+class nat_to_int_value : public const_value {
 public:
-    nat_to_int_value() {
-        m_type = Nat >> Int;
-        m_name = "nat_to_int";
-    }
-    virtual ~nat_to_int_value() {}
-    virtual expr get_type() const { return m_type; }
-    virtual bool operator==(value const & other) const { return dynamic_cast<nat_to_int_value const*>(&other) != nullptr; }
+    nat_to_int_value():const_value("nat_to_int", Nat >> Int) {}
     virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
         if (num_args == 2 && is_nat_value(args[1])) {
             r = mk_int_value(nat_value_numeral(args[1]));
@@ -412,23 +323,12 @@ public:
             return false;
         }
     }
-    virtual void display(std::ostream & out) const { out << m_name; }
-    virtual format pp() const { return format(m_name); }
-    virtual unsigned hash() const { return m_name.hash(); }
 };
 MK_BUILTIN(nat_to_int_fn, nat_to_int_value);
 
-class int_to_real_value : public value {
-    expr m_type;
-    name m_name;
+class int_to_real_value : public const_value {
 public:
-    int_to_real_value() {
-        m_type = Int >> Real;
-        m_name = "int_to_real";
-    }
-    virtual ~int_to_real_value() {}
-    virtual expr get_type() const { return m_type; }
-    virtual bool operator==(value const & other) const { return dynamic_cast<int_to_real_value const*>(&other) != nullptr; }
+    int_to_real_value():const_value("int_to_real", Int >> Real) {}
     virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
         if (num_args == 2 && is_int_value(args[1])) {
             r = mk_real_value(mpq(int_value_numeral(args[1])));
@@ -437,9 +337,6 @@ public:
             return false;
         }
     }
-    virtual void display(std::ostream & out) const { out << m_name; }
-    virtual format pp() const { return format(m_name); }
-    virtual unsigned hash() const { return m_name.hash(); }
 };
 MK_BUILTIN(int_to_real_fn,  int_to_real_value);
 MK_CONSTANT(nat_to_real_fn, name("nat_to_real"));
diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp
index c1c8f62b2..c8b6758f3 100644
--- a/src/kernel/builtin.cpp
+++ b/src/kernel/builtin.cpp
@@ -63,11 +63,7 @@ class bool_type_value : public value {
 public:
     virtual ~bool_type_value() {}
     virtual expr get_type() const { return Type(); }
-    virtual bool normalize(unsigned num_args, expr const * args, expr & r) const { return false; }
-    virtual bool operator==(value const & other) const { return dynamic_cast<bool_type_value const*>(&other) != nullptr; }
-    virtual void display(std::ostream & out) const { out << g_Bool_name; }
-    virtual format pp() const { return g_Bool_fmt; }
-    virtual unsigned hash() const { return g_Bool_name.hash(); }
+    virtual name get_name() const { return g_Bool_name; }
 };
 expr const Bool = mk_value(*(new bool_type_value()));
 expr mk_bool_type() { return Bool; }
@@ -79,22 +75,21 @@ static char const * g_true_u_str  = "\u22A4";
 static char const * g_false_u_str = "\u22A5";
 static format g_true_u_fmt(g_true_u_str);
 static format g_false_u_fmt(g_false_u_str);
-static char const * g_true_str  = "true";
-static char const * g_false_str = "false";
-static format g_true_fmt(g_true_str);
-static format g_false_fmt(g_false_str);
+static name g_true_name("true");
+static name g_false_name("false");
+static format g_true_fmt(g_true_name);
+static format g_false_fmt(g_false_name);
 class bool_value_value : public value {
     bool m_val;
 public:
     bool_value_value(bool v):m_val(v) {}
     virtual ~bool_value_value() {}
     virtual expr get_type() const { return Bool; }
-    virtual bool normalize(unsigned num_args, expr const * args, expr & r) const { return false; }
+    virtual name get_name() const { return m_val ? g_true_name : g_false_name; }
     virtual bool operator==(value const & other) const {
         bool_value_value const * _other = dynamic_cast<bool_value_value const*>(&other);
         return _other && _other->m_val == m_val;
     }
-    virtual void display(std::ostream & out) const { out << (m_val ? g_true_str : g_false_str); }
     virtual format pp(bool unicode) const {
         if (unicode)
             return m_val ? g_true_u_fmt : g_false_u_fmt;
@@ -102,7 +97,6 @@ public:
             return m_val ? g_true_fmt : g_false_fmt;
     }
     virtual format pp() const { return pp(true); }
-    virtual unsigned hash() const { return m_val ? 3 : 5; }
     bool get_val() const { return m_val; }
 };
 expr const True  = mk_value(*(new bool_value_value(true)));
@@ -139,6 +133,7 @@ public:
     }
     virtual ~ite_fn_value() {}
     virtual expr get_type() const { return m_type; }
+    virtual name get_name() const { return g_ite_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]))
@@ -153,10 +148,6 @@ public:
             return false;
         }
     }
-    virtual bool operator==(value const & other) const { return dynamic_cast<ite_fn_value const*>(&other) != nullptr; }
-    virtual void display(std::ostream & out) const { out << g_ite_name; }
-    virtual format pp() const { return g_ite_fmt; }
-    virtual unsigned hash() const { return g_ite_name.hash(); }
 };
 MK_BUILTIN(ite_fn, ite_fn_value);
 // =======================================
diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index bbc22c668..071ef1333 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -80,33 +80,33 @@ expr_eq::expr_eq(expr const & lhs, expr const & rhs):
     m_lhs(lhs),
     m_rhs(rhs) {
 }
-expr_eq::~expr_eq() {
-}
+expr_eq::~expr_eq() {}
 expr_abstraction::expr_abstraction(expr_kind k, name const & n, expr const & t, expr const & b):
     expr_cell(k, ::lean::hash(t.hash(), b.hash())),
     m_name(n),
     m_domain(t),
     m_body(b) {
 }
-expr_lambda::expr_lambda(name const & n, expr const & t, expr const & e):
-    expr_abstraction(expr_kind::Lambda, n, t, e) {}
-expr_pi::expr_pi(name const & n, expr const & t, expr const & e):
-    expr_abstraction(expr_kind::Pi, n, t, e) {}
-
+expr_lambda::expr_lambda(name const & n, expr const & t, expr const & e):expr_abstraction(expr_kind::Lambda, n, t, e) {}
+expr_pi::expr_pi(name const & n, expr const & t, expr const & e):expr_abstraction(expr_kind::Pi, n, t, e) {}
 expr_type::expr_type(level const & l):
     expr_cell(expr_kind::Type, l.hash()),
     m_level(l) {
 }
-expr_type::~expr_type() {
-}
+expr_type::~expr_type() {}
 expr_let::expr_let(name const & n, expr const & v, expr const & b):
     expr_cell(expr_kind::Let, ::lean::hash(v.hash(), b.hash())),
     m_name(n),
     m_value(v),
     m_body(b) {
 }
-expr_let::~expr_let() {
-}
+expr_let::~expr_let() {}
+bool value::normalize(unsigned num_args, expr const * args, expr & r) const { return false; }
+void value::display(std::ostream & out) const { out << get_name(); }
+bool value::operator==(value const & other) const { return typeid(*this) == typeid(other); }
+format value::pp() const { return format(get_name()); }
+format value::pp(bool unicode) const { return pp(); }
+unsigned value::hash() const { return get_name().hash(); }
 expr_value::expr_value(value & v):
     expr_cell(expr_kind::Value, v.hash()),
     m_val(v) {
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index 00f52bda0..349c675ba 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -204,12 +204,13 @@ public:
     value():m_rc(0) {}
     virtual ~value() {}
     virtual expr get_type() const = 0;
-    virtual bool normalize(unsigned num_args, expr const * args, expr & r) const = 0;
-    virtual bool operator==(value const & other) const = 0;
-    virtual void display(std::ostream & out) const = 0;
-    virtual format pp() const = 0;
-    virtual format pp(bool unicode) const { return pp(); }
-    virtual unsigned hash() const = 0;
+    virtual name get_name() const = 0;
+    virtual bool normalize(unsigned num_args, expr const * args, expr & r) const;
+    virtual bool operator==(value const & other) const;
+    virtual void display(std::ostream & out) const;
+    virtual format pp() const;
+    virtual format pp(bool unicode) const;
+    virtual unsigned hash() const;
 };
 /** \brief Semantic attachments */
 class expr_value : public expr_cell {
@@ -223,7 +224,6 @@ public:
 };
 // =======================================
 
-
 // =======================================
 // Testers
 inline bool is_var(expr_cell * e)         { return e->kind() == expr_kind::Var; }
diff --git a/src/kernel/level.h b/src/kernel/level.h
index 2eb1f4800..a59c898a5 100644
--- a/src/kernel/level.h
+++ b/src/kernel/level.h
@@ -63,10 +63,13 @@ inline bool is_uvar(level const & l) { return kind(l) == level_kind::UVar;  }
 inline bool is_lift(level const & l) { return kind(l) == level_kind::Lift; }
 inline bool is_max (level const & l) { return kind(l) == level_kind::Max;  }
 
+/** \brief Return a */
 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); }
 
+/** \brief Pretty print the given level expression, unicode characters are used if \c unicode is \c true. */
 format pp(level const & l, bool unicode);
+/** \brief Pretty print the given level expression using the given configuration options. */
 format pp(level const & l, options const & opts = options());
 }
 void print(lean::level const & l);
diff --git a/src/kernel/value.h b/src/kernel/value.h
new file mode 100644
index 000000000..628b50790
--- /dev/null
+++ b/src/kernel/value.h
@@ -0,0 +1,33 @@
+/*
+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"
+
+namespace lean {
+// Some value subclasses that capture common implementation patterns.
+class named_value : public value {
+    name m_name;
+public:
+    named_value(name const & n):m_name(n) {}
+    virtual ~named_value() {}
+    virtual name get_name() const { return m_name; }
+};
+
+class const_value : public named_value {
+    expr m_type;
+public:
+    const_value(name const & n, expr const & t):named_value(n), m_type(t) {}
+    virtual ~const_value() {}
+    virtual expr get_type() const { return m_type; }
+};
+
+class type_value : public named_value {
+public:
+    type_value(name const & n):named_value(n) {}
+    virtual expr get_type() const { return Type(); }
+};
+}
diff --git a/src/library/context_to_lambda.h b/src/library/context_to_lambda.h
index 175764d68..0f2618bf8 100644
--- a/src/library/context_to_lambda.h
+++ b/src/library/context_to_lambda.h
@@ -23,14 +23,12 @@ namespace lean {
    value V_i, then we just use (fake T_i).
 */
 expr context_to_lambda(context const & c, expr const & e);
-
 /**
    \brief Return true if \c e is a fake context created using
    context_to_lambda.
    (lambda (n_1 : (fake T_1 V_1)) ... (lambda (n_k : (fake T_k V_k)) e))
 */
 bool is_fake_context(expr const & e);
-
 /**
    \brief Return the name n_1 of the head of the (fake) context
    (lambda (n_1 : (fake T_1 V_1)) ... (lambda (n_k : (fake T_k V_k)) e))
@@ -38,7 +36,6 @@ bool is_fake_context(expr const & e);
    \pre is_fake_context(e)
 */
 name const & fake_context_name(expr const & e);
-
 /**
    \brief Return the domain T_1 of the head of the (fake) context
    (lambda (n_1 : (fake T_1 V_1)) ... (lambda (n_k : (fake T_k V_k)) e))
@@ -46,7 +43,6 @@ name const & fake_context_name(expr const & e);
    \pre is_fake_context(e)
 */
 expr const & fake_context_domain(expr const & e);
-
 /**
    \brief Return the value V_1 of the head of the (fake) context
    (lambda (n_1 : (fake T_1 V_1)) ... (lambda (n_k : (fake T_k V_k)) e))
diff --git a/src/library/formatter.h b/src/library/formatter.h
index 254eff420..6bbdb18a2 100644
--- a/src/library/formatter.h
+++ b/src/library/formatter.h
@@ -38,6 +38,9 @@ public:
     virtual void set_interrupt(bool flag) {}
 };
 class kernel_exception;
+/**
+   \brief Smart-pointer for the actual formatter object (aka \c formatter_cell).
+*/
 class formatter {
     std::shared_ptr<formatter_cell> m_cell;
 public:
@@ -52,6 +55,8 @@ public:
     format operator()(kernel_exception const & ex, options const & opts = options());
     void set_interrupt(bool flag) { m_cell->set_interrupt(flag); }
 };
-
+/**
+   \brief Create a simple formatter object based on #printer class.
+*/
 formatter mk_simple_formatter();
 }
diff --git a/src/library/printer.cpp b/src/library/printer.cpp
index a995deb83..b5645fead 100644
--- a/src/library/printer.cpp
+++ b/src/library/printer.cpp
@@ -21,6 +21,10 @@ bool is_atomic(expr const & e) {
     return false;
 }
 
+/**
+   \brief Very basic printer for expressions.
+   It is mainly used when debugging code.
+*/
 struct print_expr_fn {
     std::ostream & m_out;
 
diff --git a/src/util/list.h b/src/util/list.h
index e950851f6..d19158a64 100644
--- a/src/util/list.h
+++ b/src/util/list.h
@@ -43,13 +43,16 @@ public:
     list & operator=(list const & s) { LEAN_COPY_REF(list, s); }
     list & operator=(list && s) { LEAN_MOVE_REF(list, s); }
 
+    /** \brief Return true iff it is not the empty/nil list. */
     operator bool() const { return m_ptr != nullptr; }
 
     friend bool is_nil(list const & l) { return l.m_ptr == nullptr; }
     friend T const & head(list const & l) { lean_assert(!is_nil(l)); return l.m_ptr->m_head; }
     friend list const & tail(list const & l) { lean_assert(!is_nil(l)); return l.m_ptr->m_tail; }
 
+    /** \brief Pointer equality. Return true iff \c l1 and \c l2 point to the same memory location. */
     friend bool is_eqp(list const & l1, list const & l2) { return l1.m_ptr == l2.m_ptr; }
+    /** \brief Structural equality. */
     friend bool operator==(list const & l1, list const & l2) {
         cell * it1 = l1.m_ptr;
         cell * it2 = l2.m_ptr;
diff --git a/src/util/name.h b/src/util/name.h
index ecb39eddf..ad869c280 100644
--- a/src/util/name.h
+++ b/src/util/name.h
@@ -26,6 +26,11 @@ public:
     name(name const & prefix, unsigned k);
     name(name const & other);
     name(name && other);
+    /**
+       \brief Create a hierarchical name using the given strings.
+       Example: <code>name{"foo", "bla", "tst"}</code> creates the hierarchical
+       name <tt>foo::bla::tst</tt>.
+    */
     name(std::initializer_list<char const *> const & l);
     ~name();
     static name const & anonymous();
@@ -37,7 +42,9 @@ public:
     friend bool operator!=(name const & a, name const & b) { return !(a == b); }
     friend bool operator==(name const & a, char const * b);
     friend bool operator!=(name const & a, char const * b) { return !(a == b); }
-    // total order on hierarchical names.
+    /**
+        \brief Total order on hierarchical names.
+    */
     friend int cmp(name const & a, name const & b) { return cmp(a.m_ptr, b.m_ptr); }
     friend bool operator<(name const & a, name const & b) { return cmp(a, b) < 0; }
     friend bool operator>(name const & a, name const & b) { return cmp(a, b) > 0; }
@@ -48,12 +55,18 @@ public:
     bool is_string() const    { return kind() == name_kind::STRING; }
     bool is_numeral() const   { return kind() == name_kind::NUMERAL; }
     unsigned get_numeral() const;
+    /**
+       \brief If the tail of the given hierarchical name is a string, then it returns this string.
+       \pre is_string()
+    */
     char const * get_string() const;
     bool is_atomic() const;
-    name get_prefix() const;
     /**
-       \brief Convert this hierarchical name into a string.
+        \brief Return the prefix of a hierarchical name
+        \pre !is_atomic()
     */
+    name get_prefix() const;
+    /** \brief Convert this hierarchical name into a string. */
     std::string to_string() const;
     /** \brief Size of the this name (in characters). */
     size_t size() const;
diff --git a/src/util/sexpr/sexpr.h b/src/util/sexpr/sexpr.h
index e2ee2f701..eb2a6f09f 100644
--- a/src/util/sexpr/sexpr.h
+++ b/src/util/sexpr/sexpr.h
@@ -144,6 +144,9 @@ template<typename T> inline bool operator==(T const & a, sexpr const & b) { retu
 inline bool operator!=(sexpr const & a, sexpr const & b) { return !(a == b); }
 template<typename T> inline bool operator!=(sexpr const & a, T const & b) { return !(a == b); }
 template<typename T> inline bool operator!=(T const & a, sexpr const & b) { return !(a == b); }
+/**
+   \brief Total order on S-expressions.
+*/
 int cmp(sexpr const & a, sexpr const & b);
 inline bool operator<(sexpr const & a, sexpr const & b) { return cmp(a, b) < 0; }
 inline bool operator>(sexpr const & a, sexpr const & b) { return cmp(a, b) > 0; }