diff --git a/library/init/core.lean b/library/init/core.lean
index 8420f92b10..feb3ebb647 100644
--- a/library/init/core.lean
+++ b/library/init/core.lean
@@ -2127,7 +2127,7 @@ namespace classical
 
 axiom choice {α : Sort u} : nonempty α → α
 
-noncomputable theorem indefinite_description {α : Sort u} (p : α → Prop)
+noncomputable def indefinite_description {α : Sort u} (p : α → Prop)
   (h : ∃ x, p x) : {x // p x} :=
 choice $ let ⟨x, px⟩ := h in ⟨⟨x, px⟩⟩
 
@@ -2214,7 +2214,7 @@ match (prop_decidable (nonempty α)) with
 | (is_true hp)  := psum.inl (@inhabited.default _ (inhabited_of_nonempty hp))
 | (is_false hn) := psum.inr (λ a, absurd (nonempty.intro a) hn)
 
-noncomputable theorem strong_indefinite_description {α : Sort u} (p : α → Prop)
+noncomputable def strong_indefinite_description {α : Sort u} (p : α → Prop)
   (h : nonempty α) : {x : α // (∃ y : α, p y) → p x} :=
 if hp : ∃ x : α, p x then
   let xp := indefinite_description _ hp in
diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp
index b37ebb5941..fe49a82099 100644
--- a/src/frontends/lean/definition_cmds.cpp
+++ b/src/frontends/lean/definition_cmds.cpp
@@ -487,9 +487,9 @@ static void check_example(environment const & decl_env, options const & opts,
 
         bool is_meta      = modifiers.m_is_meta;
         auto new_env = elab.env();
-        auto def = mk_definition(new_env, decl_name, names(univ_params_buf), type, val, is_meta);
+        declaration def = mk_definition(new_env, decl_name, names(univ_params_buf), type, val, is_meta);
         new_env = module::add(new_env, def);
-        check_noncomputable(noncomputable_theory, new_env, decl_name, def.get_name(), modifiers.m_is_noncomputable,
+        check_noncomputable(noncomputable_theory, new_env, decl_name, decl_name, modifiers.m_is_noncomputable,
                                  pos_provider.get_file_name(), pos_provider.get_some_pos());
     } catch (throwable & ex) {
         message_builder error_msg(tc, decl_env, get_global_ios(),
diff --git a/src/frontends/lean/inductive_cmds.cpp b/src/frontends/lean/inductive_cmds.cpp
index 15559f701c..fc2838df12 100644
--- a/src/frontends/lean/inductive_cmds.cpp
+++ b/src/frontends/lean/inductive_cmds.cpp
@@ -756,13 +756,11 @@ public:
 };
 
 void parse_inductive_decl(parser & p, cmd_meta const & meta) {
-    auto pos = p.pos();
     inductive_cmd_fn(p, meta).parse_and_elaborate();
 }
 
 environment inductive_cmd(parser & p, cmd_meta const & meta) {
     p.next();
-    auto pos = p.pos();
     return inductive_cmd_fn(p, meta).inductive_cmd();
 }
 
diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp
index 018f4ddbbb..2fc15d9eb1 100644
--- a/src/frontends/lean/util.cpp
+++ b/src/frontends/lean/util.cpp
@@ -476,7 +476,7 @@ void initialize_frontend_lean_util() {
     g_field_notation_name   = new name("field_notation");
 }
 
-environment compile_expr(environment const & env, name const & n, level_param_names const & ls, expr const & type, expr const & e, pos_info const & pos) {
+environment compile_expr(environment const & env, name const & n, level_param_names const & ls, expr const & type, expr const & e, pos_info const & /* pos */) {
     environment new_env = env;
     bool is_meta        = true;
     new_env = new_env.add(mk_definition(new_env, n, ls, type, e, is_meta));
diff --git a/src/kernel/declaration.cpp b/src/kernel/declaration.cpp
index abb11b8662..a2d72f6489 100644
--- a/src/kernel/declaration.cpp
+++ b/src/kernel/declaration.cpp
@@ -37,14 +37,32 @@ int compare(reducibility_hints const & h1, reducibility_hints const & h2) {
     }
 }
 
-recursor_rule::recursor_rule(name const & cnstr, unsigned nfields, expr const & rhs):
-    object_ref(mk_cnstr(0, cnstr.raw(), mk_nat_obj(nfields), rhs.raw())) {
-    inc(cnstr.raw());
-    inc(rhs.raw());
+constant_val::constant_val(name const & n, level_param_names const & lparams, expr const & type):
+    object_ref(mk_cnstr(0, n, lparams, type)) {
+}
+
+axiom_val::axiom_val(name const & n, level_param_names const & lparams, expr const & type, bool is_meta):
+    object_ref(mk_cnstr(0, constant_val(n, lparams, type), 1)) {
+    cnstr_set_scalar<unsigned char>(raw(), sizeof(object*), static_cast<unsigned char>(is_meta));
+}
+
+bool axiom_val::is_meta() const { return cnstr_scalar<unsigned char>(raw(), sizeof(object*)) != 0; }
+
+definition_val::definition_val(name const & n, level_param_names const & lparams, expr const & type, expr const & val, reducibility_hints const & hints, bool is_meta):
+    object_ref(mk_cnstr(0, constant_val(n, lparams, type), val, hints, 1)) {
+    cnstr_set_scalar<unsigned char>(raw(), sizeof(object*)*3, static_cast<unsigned char>(is_meta));
+}
+
+bool definition_val::is_meta() const { return cnstr_scalar<unsigned char>(raw(), sizeof(object*)*3) != 0; }
+
+theorem_val::theorem_val(name const & n, level_param_names const & lparams, expr const & type, expr const & val):
+    object_ref(mk_cnstr(0, constant_val(n, lparams, type), val)) {
+}
+
+recursor_rule::recursor_rule(name const & cnstr, unsigned nfields, expr const & rhs):
+    object_ref(mk_cnstr(0, cnstr, nat(nfields), rhs)) {
 }
 
-static unsigned definition_scalar_offset() { return sizeof(object*)*3; }
-static unsigned axiom_scalar_offset() { return sizeof(object*); }
 static unsigned inductive_scalar_offset() { return sizeof(object*)*6; }
 static unsigned constructor_scalar_offset() { return sizeof(object*)*3; }
 static unsigned recursor_scalar_offset() { return sizeof(object*)*7; }
@@ -55,97 +73,18 @@ bool constructor_val::is_meta() const { return cnstr_scalar<unsigned char>(raw()
 bool recursor_val::is_k() const { return (cnstr_scalar<unsigned char>(raw(), recursor_scalar_offset()) & 1) != 0; }
 bool recursor_val::is_meta() const { return (cnstr_scalar<unsigned char>(raw(), recursor_scalar_offset()) & 2) != 0; }
 
-static object * mk_declaration_val(name const & n, level_param_names const & params, expr const & t) {
-    object * r = alloc_cnstr(0, 3, 0);
-    inc(n.raw());      cnstr_set_obj(r, 0, n.raw());
-    inc(params.raw()); cnstr_set_obj(r, 1, params.raw());
-    inc(t.raw());      cnstr_set_obj(r, 2, t.raw());
-    return r;
-}
-
-static object * mk_axiom_val(name const & n, level_param_names const & params, expr const & t, bool meta) {
-    object * r = alloc_cnstr(0, 1, sizeof(unsigned char));
-    cnstr_set_obj(r, 0, mk_declaration_val(n, params, t));
-    cnstr_set_scalar<unsigned char>(r, axiom_scalar_offset(), static_cast<unsigned char>(meta));
-    return r;
-}
-
-static object * mk_definition_val(name const & n, level_param_names const & params, expr const & t, expr const & v,
-                                  reducibility_hints const & h, bool meta) {
-    object * r = alloc_cnstr(0, 3, sizeof(unsigned char));
-    cnstr_set_obj(r, 0, mk_declaration_val(n, params, t));
-    inc(v.raw()); cnstr_set_obj(r, 1, v.raw());
-    inc(h.raw()); cnstr_set_obj(r, 2, h.raw());
-    cnstr_set_scalar<unsigned char>(r, definition_scalar_offset(), static_cast<unsigned char>(meta));
-    return r;
-}
-
-static object * mk_theorem_val(name const & n, level_param_names const & params, expr const & t, expr const & v) {
-    object * r = alloc_cnstr(0, 2, 0);
-    cnstr_set_obj(r, 0, mk_declaration_val(n, params, t));
-    inc(v.raw()); cnstr_set_obj(r, 1, v.raw());
-    return r;
-}
-
-static object * mk_inductive_val(name const & n, level_param_names const & params, expr const & t, unsigned nparams, unsigned nindices,
-                                 names const & all, names const & cnstrs, names const & recs, bool is_rec, bool is_meta) {
-    object * r = alloc_cnstr(0, 6, 1);
-    cnstr_set_obj(r, 0, mk_declaration_val(n, params, t));
-    cnstr_set_obj(r, 1, mk_nat_obj(nparams));
-    cnstr_set_obj(r, 2, mk_nat_obj(nindices));
-    inc(all.raw()); cnstr_set_obj(r, 3, all.raw());
-    inc(cnstrs.raw()); cnstr_set_obj(r, 4, cnstrs.raw());
-    inc(recs.raw()); cnstr_set_obj(r, 5, recs.raw());
-    cnstr_set_scalar<unsigned char>(r, inductive_scalar_offset(), (is_rec ? 1 : 0) + (is_meta ? 2 : 0));
-    return r;
-}
-
-static object * mk_constructor_val(name const & n, level_param_names const & params, expr const & t, name const & induct, unsigned nparams,
-                                   bool is_meta) {
-    object * r = alloc_cnstr(0, 3, 1);
-    cnstr_set_obj(r, 0, mk_declaration_val(n, params, t));
-    inc(induct.raw()); cnstr_set_obj(r, 1, induct.raw());
-    cnstr_set_obj(r, 2, mk_nat_obj(nparams));
-    cnstr_set_scalar<unsigned char>(r, inductive_scalar_offset(), static_cast<unsigned char>(is_meta));
-    return r;
-}
-
-static object * mk_recursor_val(name const & n, level_param_names const & params, expr const & t, name const & induct, unsigned nparams,
-                                unsigned nindices, unsigned nmotives, unsigned nminor, bool k, recursor_rules const & rules, bool is_meta) {
-    object * r = alloc_cnstr(0, 7, 1);
-    cnstr_set_obj(r, 0, mk_declaration_val(n, params, t));
-    cnstr_set_obj(r, 0, mk_declaration_val(n, params, t));
-    inc(induct.raw()); cnstr_set_obj(r, 1, induct.raw());
-    cnstr_set_obj(r, 2, mk_nat_obj(nparams));
-    cnstr_set_obj(r, 3, mk_nat_obj(nindices));
-    cnstr_set_obj(r, 4, mk_nat_obj(nmotives));
-    cnstr_set_obj(r, 5, mk_nat_obj(nminor));
-    inc(rules.raw()); cnstr_set_obj(r, 6, rules.raw());
-    cnstr_set_scalar<unsigned char>(r, recursor_scalar_offset(), (k ? 1 : 0) + (is_meta ? 2 : 0));
-    return r;
-}
-
 bool declaration::is_meta() const {
     switch (kind()) {
-    case declaration_kind::Definition:  return cnstr_scalar<unsigned char>(get_val_obj(), definition_scalar_offset()) != 0;
-    case declaration_kind::Axiom:       return cnstr_scalar<unsigned char>(get_val_obj(), axiom_scalar_offset()) != 0;
-    case declaration_kind::Theorem:     return false;
-    case declaration_kind::Inductive:   lean_unreachable(); // TODO(Leo):
-    case declaration_kind::Quot:        return false;
+    case declaration_kind::Definition:       return to_definition_val().is_meta();
+    case declaration_kind::Axiom:            return to_axiom_val().is_meta();
+    case declaration_kind::Theorem:          return false;
+    case declaration_kind::Inductive:        lean_unreachable(); // TODO(Leo):
+    case declaration_kind::Quot:             return false;
     case declaration_kind::MutualDefinition: return true;
     }
     lean_unreachable();
 }
 
-static reducibility_hints * g_opaque = nullptr;
-
-reducibility_hints const & declaration::get_hints() const {
-    if (is_definition())
-        return static_cast<reducibility_hints const &>(cnstr_obj_ref(to_val(), 2));
-    else
-        return *g_opaque;
-}
-
 bool use_meta(environment const & env, expr const & e) {
     bool found = false;
     for_each(e, [&](expr const & e, unsigned) {
@@ -168,7 +107,7 @@ declaration::declaration():declaration(*g_dummy) {}
 
 declaration mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v,
                           reducibility_hints const & h, bool meta) {
-    return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Definition), mk_definition_val(n, params, t, v, h, meta)));
+    return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Definition), definition_val(n, params, t, v, h, meta)));
 }
 
 static unsigned get_max_height(environment const & env, expr const & v) {
@@ -191,11 +130,11 @@ declaration mk_definition(environment const & env, name const & n, level_param_n
 }
 
 declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v) {
-    return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Theorem), mk_theorem_val(n, params, t, v)));
+    return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Theorem), theorem_val(n, params, t, v)));
 }
 
 declaration mk_axiom(name const & n, level_param_names const & params, expr const & t, bool meta) {
-    return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Axiom), mk_axiom_val(n, params, t, meta)));
+    return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Axiom), axiom_val(n, params, t, meta)));
 }
 
 declaration mk_definition_inferring_meta(environment const & env, name const & n, level_param_names const & params,
@@ -222,16 +161,13 @@ declaration mk_quot_decl(name const & n) {
 }
 
 inductive_type::inductive_type(name const & id, expr const & type, constructors const & cnstrs):
-    object_ref(mk_cnstr(0, id.raw(), type.raw(), cnstrs.raw())) {
-    inc(id.raw()); inc(type.raw()); inc(cnstrs.raw());
+    object_ref(mk_cnstr(0, id, type, cnstrs)) {
 }
 
 static unsigned inductive_decl_scalar_offset() { return sizeof(object*)*3; }
 
 declaration mk_inductive_decl(names const & lparams, nat const & nparams, inductive_types const & types, bool is_meta) {
-    declaration r(mk_cnstr(static_cast<unsigned>(declaration_kind::Inductive),
-                           lparams.raw(), nparams.raw(), types.raw(), 1));
-    inc(lparams.raw()); inc(nparams.raw()); inc(types.raw());
+    declaration r(mk_cnstr(static_cast<unsigned>(declaration_kind::Inductive), lparams, nparams, types, 1));
     cnstr_set_scalar<unsigned char>(r.raw(), inductive_decl_scalar_offset(), static_cast<unsigned char>(is_meta));
     return r;
 }
@@ -247,6 +183,8 @@ constant_info::constant_info(declaration const & d):object_ref(d.raw()) {
     inc_ref(d.raw());
 }
 
+static reducibility_hints * g_opaque = nullptr;
+
 reducibility_hints const & constant_info::get_hints() const {
     if (is_definition())
         return static_cast<reducibility_hints const &>(cnstr_obj_ref(to_val(), 2));
@@ -256,13 +194,13 @@ reducibility_hints const & constant_info::get_hints() const {
 
 bool constant_info::is_meta() const {
     switch (kind()) {
-    case constant_info_kind::Definition:  return cnstr_scalar<unsigned char>(get_val_obj(), definition_scalar_offset()) != 0;
+    case constant_info_kind::Axiom:       return to_axiom_val().is_meta();
+    case constant_info_kind::Definition:  return to_definition_val().is_meta();
+    case constant_info_kind::Theorem:     return false;
     case constant_info_kind::Inductive:   return false; // TODO(Leo): to_inductive_val().is_meta();
     case constant_info_kind::Quot:        return false;
     case constant_info_kind::Constructor: return false; // TODO(Leo): to_constructor_val().is_meta();
     case constant_info_kind::Recursor:    return false; // TODO(Leo): to_recursor_val().is_meta();
-    case constant_info_kind::Axiom:       return cnstr_scalar<unsigned char>(get_val_obj(), axiom_scalar_offset()) != 0;
-    case constant_info_kind::Theorem:     return false;
     }
     lean_unreachable();
 }
diff --git a/src/kernel/declaration.h b/src/kernel/declaration.h
index 087aad90bd..ad77327f8f 100644
--- a/src/kernel/declaration.h
+++ b/src/kernel/declaration.h
@@ -63,20 +63,77 @@ inline deserializer & operator>>(deserializer & d, reducibility_hints & l) { l =
 int compare(reducibility_hints const & h1, reducibility_hints const & h2);
 
 /*
-structure declaration_val :=
+structure constant_val :=
 (id : name) (lparams : list name) (type : expr)
 */
-class declaration_val : public object_ref {
+class constant_val : public object_ref {
 public:
-    declaration_val(declaration_val const & other):object_ref(other) {}
-    declaration_val(declaration_val && other):object_ref(other) {}
-    declaration_val & operator=(declaration_val const & other) { object_ref::operator=(other); return *this; }
-    declaration_val & operator=(declaration_val && other) { object_ref::operator=(other); return *this; }
+    constant_val(name const & n, level_param_names const & lparams, expr const & type);
+    constant_val(constant_val const & other):object_ref(other) {}
+    constant_val(constant_val && other):object_ref(other) {}
+    constant_val & operator=(constant_val const & other) { object_ref::operator=(other); return *this; }
+    constant_val & operator=(constant_val && other) { object_ref::operator=(other); return *this; }
     name const & get_name() const { return static_cast<name const &>(cnstr_obj_ref(*this, 0)); }
     level_param_names const & get_lparams() const { return static_cast<level_param_names const &>(cnstr_obj_ref(*this, 1)); }
     expr const & get_type() const { return static_cast<expr const &>(cnstr_obj_ref(*this, 2)); }
 };
 
+/*
+structure axiom_val extends constant_val :=
+(is_meta : bool)
+*/
+class axiom_val : public object_ref {
+public:
+    axiom_val(name const & n, level_param_names const & lparams, expr const & type, bool is_meta);
+    axiom_val(axiom_val const & other):object_ref(other) {}
+    axiom_val(axiom_val && other):object_ref(other) {}
+    axiom_val & operator=(axiom_val const & other) { object_ref::operator=(other); return *this; }
+    axiom_val & operator=(axiom_val && other) { object_ref::operator=(other); return *this; }
+    constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_obj_ref(*this, 0)); }
+    name const & get_name() const { return to_constant_val().get_name(); }
+    level_param_names const & get_lparams() const { return to_constant_val().get_lparams(); }
+    expr const & get_type() const { return to_constant_val().get_type(); }
+    bool is_meta() const;
+};
+
+/*
+structure definition_val extends constant_val :=
+(value : expr) (hints : reducibility_hints) (is_meta : bool)
+*/
+class definition_val : public object_ref {
+public:
+    definition_val(name const & n, level_param_names const & lparams, expr const & type, expr const & val, reducibility_hints const & hints, bool is_meta);
+    definition_val(definition_val const & other):object_ref(other) {}
+    definition_val(definition_val && other):object_ref(other) {}
+    definition_val & operator=(definition_val const & other) { object_ref::operator=(other); return *this; }
+    definition_val & operator=(definition_val && other) { object_ref::operator=(other); return *this; }
+    constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_obj_ref(*this, 0)); }
+    name const & get_name() const { return to_constant_val().get_name(); }
+    level_param_names const & get_lparams() const { return to_constant_val().get_lparams(); }
+    expr const & get_type() const { return to_constant_val().get_type(); }
+    expr const & get_value() const { return static_cast<expr const &>(cnstr_obj_ref(*this, 1)); }
+    reducibility_hints const & get_hints() const { return static_cast<reducibility_hints const &>(cnstr_obj_ref(*this, 2)); }
+    bool is_meta() const;
+};
+
+/*
+structure theorem_val extends constant_val :=
+(value : task expr)
+*/
+class theorem_val : public object_ref {
+public:
+    theorem_val(name const & n, level_param_names const & lparams, expr const & type, expr const & val);
+    theorem_val(theorem_val const & other):object_ref(other) {}
+    theorem_val(theorem_val && other):object_ref(other) {}
+    theorem_val & operator=(theorem_val const & other) { object_ref::operator=(other); return *this; }
+    theorem_val & operator=(theorem_val && other) { object_ref::operator=(other); return *this; }
+    constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_obj_ref(*this, 0)); }
+    name const & get_name() const { return to_constant_val().get_name(); }
+    level_param_names const & get_lparams() const { return to_constant_val().get_lparams(); }
+    expr const & get_type() const { return to_constant_val().get_type(); }
+    expr const & get_value() const { return static_cast<expr const &>(cnstr_obj_ref(*this, 1)); }
+};
+
 /*
 structure constructor :=
 (id : name) (type : expr)
@@ -116,12 +173,6 @@ enum class declaration_kind { Axiom, Definition, Theorem, Quot, MutualDefinition
 class declaration : public object_ref {
     object * get_val_obj() const { return cnstr_obj(raw(), 0); }
     object_ref const & to_val() const { return cnstr_obj_ref(*this, 0); }
-
-    declaration_val const & to_declaration_val() const {
-        lean_assert(is_axiom() || is_definition() || is_theorem());
-        return static_cast<declaration_val const &>(cnstr_obj_ref(to_val(), 0));
-    }
-
 public:
     declaration();
     declaration(declaration const & other):object_ref(other) {}
@@ -143,12 +194,9 @@ public:
     bool is_meta() const;
     bool has_value() const { return is_theorem() || is_definition(); }
 
-    name const & get_name() const { return to_declaration_val().get_name(); }
-    level_param_names const & get_univ_params() const { return to_declaration_val().get_lparams(); }
-    unsigned get_num_univ_params() const { return length(get_univ_params()); }
-    expr const & get_type() const { return to_declaration_val().get_type(); }
-    expr const & get_value() const { lean_assert(has_value()); return static_cast<expr const &>(cnstr_obj_ref(to_val(), 1)); }
-    reducibility_hints const & get_hints() const;
+    axiom_val const & to_axiom_val() const { lean_assert(is_axiom()); return static_cast<axiom_val const &>(cnstr_obj_ref(raw(), 0)); }
+    definition_val const & to_definition_val() const { lean_assert(is_definition()); return static_cast<definition_val const &>(cnstr_obj_ref(raw(), 0)); }
+    theorem_val const & to_theorem_val() const { lean_assert(is_theorem()); return static_cast<theorem_val const &>(cnstr_obj_ref(raw(), 0)); }
 
     void serialize(serializer & s) const { s.write_object(raw()); }
     static declaration deserialize(deserializer & d) { object * o = d.read_object(); inc(o); return declaration(o); }
@@ -190,7 +238,11 @@ declaration mk_axiom_inferring_meta(environment const & env, name const & n,
     | induct_decl      (lparams : list name) (nparams : nat) (types : list inductive_type) (is_meta : bool) */
 class inductive_decl : public object_ref {
 public:
+    inductive_decl(inductive_decl const & other):object_ref(other) {}
+    inductive_decl(inductive_decl && other):object_ref(other) {}
     inductive_decl(declaration const & d):object_ref(d) { lean_assert(d.is_inductive()); }
+    inductive_decl & operator=(inductive_decl const & other) { object_ref::operator=(other); return *this; }
+    inductive_decl & operator=(inductive_decl && other) { object_ref::operator=(other); return *this; }
     names const & get_lparams() const { return static_cast<names const &>(cnstr_obj_ref(raw(), 0)); }
     nat const & get_nparams() const { return static_cast<nat const &>(cnstr_obj_ref(raw(), 1)); }
     inductive_types const & get_types() const { return static_cast<inductive_types const &>(cnstr_obj_ref(raw(), 2)); }
@@ -198,7 +250,7 @@ public:
 };
 
 /*
-structure inductive_val extends declaration_val :=
+structure inductive_val extends constant_val :=
 (nparams : nat)       -- Number of parameters
 (nindices : nat)      -- Number of indices
 (all : list name)     -- List of all (including this one) inductive datatypes in the mutual declaration containing this one
@@ -215,7 +267,7 @@ public:
     inductive_val(inductive_val && other):object_ref(other) {}
     inductive_val & operator=(inductive_val const & other) { object_ref::operator=(other); return *this; }
     inductive_val & operator=(inductive_val && other) { object_ref::operator=(other); return *this; }
-    declaration_val const & to_declaration_val() const { return static_cast<declaration_val const &>(cnstr_obj_ref(*this, 0)); }
+    constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_obj_ref(*this, 0)); }
     nat const & get_nparams() const { return static_cast<nat const &>(cnstr_obj_ref(*this, 1)); }
     nat const & get_nindices() const { return static_cast<nat const &>(cnstr_obj_ref(*this, 2)); }
     names const & get_all() const { return static_cast<names const &>(cnstr_obj_ref(*this, 3)); }
@@ -226,7 +278,7 @@ public:
 };
 
 /*
-structure constructor_val extends declaration_val :=
+structure constructor_val extends constant_val :=
 (induct  : name)  -- Inductive type this constructor is a member of
 (nparams : nat)   -- Number of parameters in inductive datatype `induct`
 (is_meta : bool)
@@ -237,7 +289,7 @@ public:
     constructor_val(constructor_val && other):object_ref(other) {}
     constructor_val & operator=(constructor_val const & other) { object_ref::operator=(other); return *this; }
     constructor_val & operator=(constructor_val && other) { object_ref::operator=(other); return *this; }
-    declaration_val const & to_declaration_val() const { return static_cast<declaration_val const &>(cnstr_obj_ref(*this, 0)); }
+    constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_obj_ref(*this, 0)); }
     name const & get_induct() const { return static_cast<name const &>(cnstr_obj_ref(*this, 1)); }
     nat const & get_nparams() const { return static_cast<nat const &>(cnstr_obj_ref(*this, 2)); }
     bool is_meta() const;
@@ -264,7 +316,7 @@ public:
 typedef list_ref<recursor_rule> recursor_rules;
 
 /*
-structure recursor_val extends declaration_val :=
+structure recursor_val extends constant_val :=
 (all : list name)            -- List of all inductive datatypes in the mutual declaration that generated this recursor
 (nparams : nat)              -- Number of parameters
 (nindices : nat)             -- Number of indices
@@ -280,7 +332,7 @@ public:
     recursor_val(recursor_val && other):object_ref(other) {}
     recursor_val & operator=(recursor_val const & other) { object_ref::operator=(other); return *this; }
     recursor_val & operator=(recursor_val && other) { object_ref::operator=(other); return *this; }
-    declaration_val const & to_declaration_val() const { return static_cast<declaration_val const &>(cnstr_obj_ref(*this, 0)); }
+    constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_obj_ref(*this, 0)); }
     names const & get_all() const { return static_cast<names const &>(cnstr_obj_ref(*this, 1)); }
     nat const & get_nparams() const { return static_cast<nat const &>(cnstr_obj_ref(*this, 2)); }
     nat const & get_nindices() const { return static_cast<nat const &>(cnstr_obj_ref(*this, 3)); }
@@ -298,7 +350,7 @@ inductive quot_kind
 | lift  -- `quot.lift`
 | ind   -- `quot.ind`
 
-structure quot_val extends declaration_val :=
+structure quot_val extends constant_val :=
 (kind : quot_kind)
 */
 
@@ -317,7 +369,7 @@ enum class constant_info_kind { Axiom, Definition, Theorem, Quot, Inductive, Con
 class constant_info : public object_ref {
     object * get_val_obj() const { return cnstr_obj(raw(), 0); }
     object_ref const & to_val() const { return cnstr_obj_ref(*this, 0); }
-    declaration_val const & to_declaration_val() const { return static_cast<declaration_val const &>(cnstr_obj_ref(to_val(), 0)); }
+    constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_obj_ref(to_val(), 0)); }
 public:
     constant_info();
     constant_info(declaration const & d);
@@ -336,14 +388,18 @@ public:
     bool is_axiom() const { return kind() == constant_info_kind::Axiom; }
     bool is_theorem() const { return kind() == constant_info_kind::Theorem; }
 
-    name const & get_name() const { return to_declaration_val().get_name(); }
-    level_param_names const & get_univ_params() const { return to_declaration_val().get_lparams(); }
+    name const & get_name() const { return to_constant_val().get_name(); }
+    level_param_names const & get_univ_params() const { return to_constant_val().get_lparams(); }
     unsigned get_num_univ_params() const { return length(get_univ_params()); }
-    expr const & get_type() const { return to_declaration_val().get_type(); }
+    expr const & get_type() const { return to_constant_val().get_type(); }
     bool has_value() const { return is_theorem() || is_definition(); }
     expr const & get_value() const { lean_assert(has_value()); return static_cast<expr const &>(cnstr_obj_ref(to_val(), 1)); }
     reducibility_hints const & get_hints() const;
 
+    axiom_val const & to_axiom_val() const { lean_assert(is_axiom()); return static_cast<axiom_val const &>(cnstr_obj_ref(raw(), 0)); }
+    definition_val const & to_definition_val() const { lean_assert(is_definition()); return static_cast<definition_val const &>(cnstr_obj_ref(raw(), 0)); }
+    theorem_val const & to_theorem_val() const { lean_assert(is_theorem()); return static_cast<theorem_val const &>(cnstr_obj_ref(raw(), 0)); }
+
     // inductive_val const & to_inductive_val() const { lean_assert(is_inductive()); return static_cast<inductive_val const &>(to_val()); }
     // constructor_val const & to_constructor_val() const { lean_assert(is_constructor()); return static_cast<constructor_val const &>(to_val()); }
     // recursor_val const & to_recursor_val() const { lean_assert(is_recursor()); return static_cast<recursor_val const &>(to_val()); }
diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp
index 9e8c3c2696..9ea475637d 100644
--- a/src/kernel/environment.cpp
+++ b/src/kernel/environment.cpp
@@ -79,8 +79,7 @@ static void check_name(environment const & env, name const & n) {
         throw already_declared_exception(env, n);
 }
 
-static void check_duplicated_univ_params(environment const & env, declaration const & d) {
-    level_param_names ls = d.get_univ_params();
+static void check_duplicated_univ_params(environment const & env, level_param_names ls) {
     while (!is_nil(ls)) {
         auto const & p = head(ls);
         ls = tail(ls);
@@ -92,54 +91,59 @@ static void check_duplicated_univ_params(environment const & env, declaration co
     }
 }
 
-static void check_definition_value(environment const & env, declaration const & d, type_checker & checker) {
-    check_no_metavar_no_fvar(env, d.get_name(), d.get_value());
-    expr val_type = checker.check(d.get_value(), d.get_univ_params());
-    if (!checker.is_def_eq(val_type, d.get_type())) {
-        throw definition_type_mismatch_exception(env, d, val_type);
-    }
+static void check_constant_val(environment const & env, constant_val const & v, type_checker & checker) {
+    check_name(env, v.get_name());
+    check_duplicated_univ_params(env, v.get_lparams());
+    check_no_metavar_no_fvar(env, v.get_name(), v.get_type());
+    expr sort = checker.check(v.get_type(), v.get_lparams());
+    checker.ensure_sort(sort, v.get_type());
 }
 
-static void check_definition_value(environment const & env, declaration const & d) {
-    bool memoize = true; bool non_meta_only = !d.is_meta();
+static void check_constant_val(environment const & env, constant_val const & v, bool non_meta_only) {
+    bool memoize = true;
     type_checker checker(env, memoize, non_meta_only);
-    if (d.has_value()) {
-        check_definition_value(env, d, checker);
-    }
+    check_constant_val(env, v, checker);
 }
 
-static void check_declaration_type(environment const & env, declaration const & d, type_checker & checker) {
-    check_no_metavar_no_fvar(env, d.get_name(), d.get_type());
-    check_duplicated_univ_params(env, d);
-    expr sort = checker.check(d.get_type(), d.get_univ_params());
-    checker.ensure_sort(sort, d.get_type());
+environment environment::add_axiom(declaration const & d, bool check) const {
+    axiom_val const & v = d.to_axiom_val();
+    if (check)
+        check_constant_val(*this, v.to_constant_val(), !d.is_meta());
+    return environment(*this, insert(m_constants, v.get_name(), constant_info(d)));
 }
 
-static void check_declaration_type(environment const & env, declaration const & d) {
-    bool memoize = true; bool non_meta_only = !d.is_meta();
-    type_checker checker(env, memoize, non_meta_only);
-    check_declaration_type(env, d, checker);
-}
-
-environment environment::add_defn_thm_axiom(declaration const & d, bool check) const {
+environment environment::add_definition(declaration const & d, bool check) const {
+    definition_val const & v = d.to_definition_val();
     if (check) {
         bool memoize = true; bool non_meta_only = !d.is_meta();
-        check_name(*this, d.get_name());
         type_checker checker(*this, memoize, non_meta_only);
-        check_declaration_type(*this, d, checker);
-        if (d.has_value()) {
-            check_definition_value(*this, d, checker);
-        }
+        check_constant_val(*this, v.to_constant_val(), checker);
+        expr val_type = checker.check(v.get_value(), v.get_lparams());
+        if (!checker.is_def_eq(val_type, v.get_type()))
+            throw definition_type_mismatch_exception(*this, d, val_type);
     }
-    return environment(*this, insert(m_constants, d.get_name(), constant_info(d)));
+    return environment(*this, insert(m_constants, v.get_name(), constant_info(d)));
+}
+
+environment environment::add_theorem(declaration const & d, bool check) const {
+    theorem_val const & v = d.to_theorem_val();
+    if (check) {
+        // TODO(Leo): we must add support for handling tasks here
+        bool memoize = true; bool non_meta_only = !d.is_meta();
+        type_checker checker(*this, memoize, non_meta_only);
+        check_constant_val(*this, v.to_constant_val(), checker);
+        expr val_type = checker.check(v.get_value(), v.get_lparams());
+        if (!checker.is_def_eq(val_type, v.get_type()))
+            throw definition_type_mismatch_exception(*this, d, val_type);
+    }
+    return environment(*this, insert(m_constants, v.get_name(), constant_info(d)));
 }
 
 environment environment::add(declaration const & d, bool check) const {
     switch (d.kind()) {
-    case declaration_kind::Axiom:
-    case declaration_kind::Definition:
-    case declaration_kind::Theorem:
-        return add_defn_thm_axiom(d, check);
+    case declaration_kind::Axiom:       return add_axiom(d, check);
+    case declaration_kind::Definition:  return add_definition(d, check);
+    case declaration_kind::Theorem:     return add_theorem(d, check);
     default:
         // NOT IMPLEMENTED YET.
         lean_unreachable();
@@ -149,18 +153,31 @@ environment environment::add(declaration const & d, bool check) const {
 environment environment::add_meta(buffer<declaration> const & ds, bool check) const {
     if (!check && trust_lvl() == 0)
         throw kernel_exception(*this, "invalid meta declarations, type checking cannot be skipped at trust level 0");
+    /* Check declarations header */
+    if (check) {
+        bool memoize = true; bool non_meta_only = false;
+        type_checker checker(*this, memoize, non_meta_only);
+        for (declaration const & d : ds) {
+            definition_val const & v = d.to_definition_val();
+            if (check)
+                check_constant_val(*this, v.to_constant_val(), checker);
+        }
+    }
+    /* Add declarations */
     environment new_env = *this;
-    /* Check declarations header, and add them to new_env.m_constants */
     for (declaration const & d : ds) {
-        check_name(new_env, d.get_name());
-        if (check)
-            check_declaration_type(new_env, d);
-        new_env.m_constants.insert(d.get_name(), constant_info(d));
+        definition_val const & v = d.to_definition_val();
+        new_env.m_constants.insert(v.get_name(), constant_info(d));
     }
     /* Check actual definitions */
     if (check) {
+        bool memoize = true; bool non_meta_only = false;
+        type_checker checker(new_env, memoize, non_meta_only);
         for (declaration const & d : ds) {
-            check_definition_value(new_env, d);
+            definition_val const & v = d.to_definition_val();
+            expr val_type = checker.check(v.get_value(), v.get_lparams());
+            if (!checker.is_def_eq(val_type, v.get_type()))
+                throw definition_type_mismatch_exception(new_env, d, val_type);
         }
     }
     return new_env;
diff --git a/src/kernel/environment.h b/src/kernel/environment.h
index c0d526bfcd..0577982b5e 100644
--- a/src/kernel/environment.h
+++ b/src/kernel/environment.h
@@ -78,7 +78,9 @@ class environment {
     environment(environment const & env, extensions const & exts):
         m_header(env.m_header), m_quot_initialized(env.m_quot_initialized), m_constants(env.m_constants), m_extensions(exts) {}
 
-    environment add_defn_thm_axiom(declaration const & d, bool check) const;
+    environment add_axiom(declaration const & d, bool check) const;
+    environment add_definition(declaration const & d, bool check) const;
+    environment add_theorem(declaration const & d, bool check) const;
     environment add_quot(declaration const & d) const;
 
 public:
diff --git a/src/library/module.cpp b/src/library/module.cpp
index 61a3ff6f49..21a07356dd 100644
--- a/src/library/module.cpp
+++ b/src/library/module.cpp
@@ -282,16 +282,21 @@ environment add_and_perform(environment const & env, std::shared_ptr<modificatio
 
 environment add(environment const & env, declaration const & d) {
     environment new_env = env.add(d);
-    if (!check_computable(new_env, d.get_name()))
-        new_env = mark_noncomputable(new_env, d.get_name());
+    if (d.is_definition()) {
+        definition_val const & v = d.to_definition_val();
+        if (!check_computable(new_env, v.get_name()))
+            new_env = mark_noncomputable(new_env, v.get_name());
+    }
     return add(new_env, std::make_shared<decl_modification>(d));
 }
 
 environment add_meta(environment const & env, buffer<declaration> const & ds) {
     environment new_env = env.add_meta(ds);
     for (declaration const & d : ds) {
-        if (!check_computable(new_env, d.get_name()))
-            new_env = mark_noncomputable(new_env, d.get_name());
+        lean_assert(is_definition(d));
+        definition_val const & v = d.to_definition_val();
+        if (!check_computable(new_env, v.get_name()))
+            new_env = mark_noncomputable(new_env, v.get_name());
     }
     return add(new_env, std::make_shared<meta_decls_modification>(to_list(ds)));
 }
diff --git a/src/library/sorry.cpp b/src/library/sorry.cpp
index 6875e13643..a0fb556bb4 100644
--- a/src/library/sorry.cpp
+++ b/src/library/sorry.cpp
@@ -38,7 +38,15 @@ bool has_sorry(expr const & ex) {
 }
 
 bool has_sorry(declaration const & decl) {
-    return has_sorry(decl.get_type()) || (decl.has_value() && has_sorry(decl.get_value()));
+    switch (decl.kind()) {
+    case declaration_kind::Axiom:            return has_sorry(decl.to_axiom_val().get_type());
+    case declaration_kind::Definition:       return has_sorry(decl.to_definition_val().get_type()) || has_sorry(decl.to_definition_val().get_value());
+    case declaration_kind::Theorem:          return has_sorry(decl.to_theorem_val().get_type()) || has_sorry(decl.to_theorem_val().get_value());
+    case declaration_kind::Quot:             return false;
+    case declaration_kind::Inductive:        return false; // TODO(Leo):
+    case declaration_kind::MutualDefinition: return false; // TODO(Leo):
+    }
+    lean_unreachable();
 }
 
 bool has_sorry(constant_info const & info) {