diff --git a/src/kernel/definition.h b/src/kernel/definition.h
index b04efbcc5..c1800b7b7 100644
--- a/src/kernel/definition.h
+++ b/src/kernel/definition.h
@@ -50,6 +50,8 @@ public:
     definition & operator=(definition const & s);
     definition & operator=(definition && s);
 
+    friend bool is_eqp(definition const & d1, definition const & d2) { return d1.m_ptr == d2.m_ptr; }
+
     bool is_definition() const;
     bool is_axiom() const;
     bool is_theorem() const;
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index e72e2a689..5c7cf6964 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -5,13 +5,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "util/interrupt.h"
+#include "util/lbool.h"
+#include "util/flet.h"
 #include "kernel/type_checker.h"
 #include "kernel/expr_maps.h"
 #include "kernel/instantiate.h"
 #include "kernel/max_sharing.h"
 
 namespace lean {
-
 /** \brief Auxiliary functional object used to implement type checker. */
 struct type_checker::imp {
     environment           m_env;
@@ -22,7 +23,10 @@ struct type_checker::imp {
     name_set              m_extra_opaque;
     max_sharing_fn        m_sharing;
     expr_map<expr>        m_cache;
-    expr_map<expr>        m_whnf_cache;
+    expr_map<expr>        m_whnf_core_cache;
+
+    // temporary flags
+    bool                  m_cnstrs_enabled; // true if constraints can be generated
 
     imp(environment const & env, name_generator const & g, constraint_handler & h,
         optional<module_idx> mod_idx, bool memoize, name_set const & extra_opaque):
@@ -47,7 +51,7 @@ struct type_checker::imp {
         return !m_memoize || m_sharing.already_processed(e);
     }
 
-    /** \brief Weak head normal form core procedure. It does not perform delta reduction nor extensions. */
+    /** \brief Weak head normal form core procedure. It does not perform delta reduction nor normalization extensions. */
     expr whnf_core(expr const & e) {
         check_system("whnf");
         lean_assert(check_memoized(e));
@@ -63,8 +67,8 @@ struct type_checker::imp {
 
         // check cache
         if (m_memoize) {
-            auto it = m_whnf_cache.find(e);
-            if (it != m_whnf_cache.end())
+            auto it = m_whnf_core_cache.find(e);
+            if (it != m_whnf_core_cache.end())
                 return it->second;
         }
 
@@ -113,7 +117,7 @@ struct type_checker::imp {
         }}
 
         if (m_memoize)
-            m_whnf_cache.insert(mk_pair(e, r));
+            m_whnf_core_cache.insert(mk_pair(e, r));
         return r;
     }
 
@@ -185,5 +189,208 @@ struct type_checker::imp {
             return unfold_name_core(e, w);
         }
     }
+
+    /** \brief Auxiliary method for \c is_delta */
+    optional<definition> is_delta_core(expr const & e) {
+        if (is_constant(e)) {
+            if (auto d = m_env.find(const_name(e)))
+                if (d->is_definition() && !is_opaque(*d))
+                    return d;
+        }
+        return none_definition();
+    }
+
+    /**
+        \brief Return some definition \c d iff \c e is a target for delta-reduction, and the given definition is the one
+        to be expanded.
+    */
+    optional<definition> is_delta(expr const & e) {
+        if (is_app(e)) {
+            expr const * it = &e;
+            while (is_app(*it)) {
+                it = &(app_fn(*it));
+            }
+            return is_delta_core(*it);
+        } else {
+            return is_delta_core(e);
+        }
+    }
+
+    /**
+        \brief Weak head normal form core procedure that perform delta reduction for non-opaque constants with
+        weight greater than or equal to \c w.
+
+        This method is based on <tt>whnf_core(expr const &)</tt> and \c unfold_names.
+
+        \remark This method does not use normalization extensions attached in the environment.
+    */
+    expr whnf_core(expr e, unsigned w) {
+        while (true) {
+            expr new_e = unfold_names(whnf_core(e), w);
+            if (is_eqp(e, new_e))
+                return e;
+            e = new_e;
+        }
+    }
+
+    void add_cnstr(constraint const & c) {
+        m_chandler.add_cnstr(c);
+    }
+
+    justification get_curr_justification() {
+        // TODO(Leo)
+        return mk_assumption_justification(0);
+    }
+
+    /** \brief Cheap test for whnf (weak head normal form) just based on the kind of \c e */
+    static bool quick_is_whnf(expr const & e) {
+        switch (e.kind()) {
+        case expr_kind::Var:      case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local:
+        case expr_kind::Lambda:   case expr_kind::Pi:
+            return true;
+        case expr_kind::Constant: case expr_kind::Macro:  case expr_kind::Let:  case expr_kind::App:
+            return false;
+        }
+        lean_unreachable(); // LCOV_EXCL_LINE
+    }
+
+    bool try_eta(expr const & t, expr const & s) {
+        lean_assert(is_lambda(t));
+        lean_assert(!is_lambda(s));
+        // TODO(Leo):
+        return false;
+    }
+
+    /**
+       \brief This is an auxiliary method for is_conv. It handles the "easy cases".
+
+       If \c def_eq is true, then it checks for definitional equality.
+    */
+    lbool quick_is_conv(expr const & t, expr const & s, bool def_eq) {
+        if (t == s)
+            return l_true; // t and s are structurally equal
+        if (is_metavar(t) || is_metavar(s)) {
+            // if t or s is a metavariable, then add constraint
+            if (!m_cnstrs_enabled)
+                return l_false; // constraint creation is disabled, so return error
+            if (def_eq)
+                add_cnstr(mk_eq_cnstr(t, s, get_curr_justification()));
+            else
+                add_cnstr(mk_conv_cnstr(t, s, get_curr_justification()));
+            return l_true;
+        }
+        if (t.kind() == s.kind()) {
+            switch (t.kind()) {
+            case expr_kind::Lambda:
+                // t and s are lambda expression, then then t is convertible to s
+                // iff
+                // domain(t) is definitionally equal to domain(s)
+                // and
+                // body(t) is definitionally equal to body(s)
+                return to_lbool(is_def_eq(binder_domain(t), binder_domain(s)) && is_def_eq(binder_body(t), binder_body(s)));
+            case expr_kind::Pi:
+                // t and s are Pi expressions, then then t is convertible to s
+                // iff
+                // domain(t) is definitionally equal to domain(s)
+                // and
+                // body(t) is convertible to body(s)
+                return to_lbool(is_def_eq(binder_domain(t), binder_domain(s)) && is_conv(binder_body(t), binder_body(s), def_eq));
+            case expr_kind::Sort:
+                // t and s are Sorts
+                if (is_trivial(sort_level(t), sort_level(s)) && (!def_eq || is_trivial(sort_level(s), sort_level(t))))
+                    return l_true;
+                if (!m_cnstrs_enabled)
+                    return l_false;
+                add_cnstr(mk_level_cnstr(sort_level(t), sort_level(s), get_curr_justification()));
+                if (def_eq)
+                    add_cnstr(mk_level_cnstr(sort_level(s), sort_level(t), get_curr_justification()));
+                return l_true;
+            case expr_kind::Meta:
+                lean_unreachable(); // LCOV_EXCL_LINE
+            case expr_kind::Var: case expr_kind::Local: case expr_kind::App:
+            case expr_kind::Constant: case expr_kind::Macro:  case expr_kind::Let:
+                // We do not handle these cases in this method.
+                break;
+            }
+        }
+        return l_undef; // This is not an "easy case"
+    }
+
+    bool is_conv(expr const & t, expr const & s, bool def_eq) {
+        check_system("is_convertible");
+        lbool r = quick_is_conv(t, s, def_eq);
+        if (r != l_undef) return r == l_true;
+
+        // apply whnf (without using delta-reduction or normalizer extensions)
+        expr t_n = whnf_core(t);
+        expr s_n = whnf_core(s);
+        if (!is_eqp(t_n, t) || !is_eqp(s_n, s)) {
+            r = quick_is_conv(t_n, s_n, def_eq);
+            if (r != l_undef) return r == l_true;
+        }
+
+        // lazy delta-reduction + whnf (still not using normalizer extensions)
+        while (true) {
+            auto d_t = is_delta(t_n);
+            auto d_s = is_delta(s_n);
+            if (!d_t && !d_s) {
+                break;
+            } else if (d_t && !d_s) {
+                t_n = whnf_core(unfold_names(t_n, 0));
+            } else if (!d_t && d_s) {
+                s_n = whnf_core(unfold_names(s_n, 0));
+            } else if (d_t->get_weight() > d_s->get_weight()) {
+                t_n = whnf_core(unfold_names(t_n, d_s->get_weight() + 1));
+            } else if (d_t->get_weight() < d_s->get_weight()) {
+                s_n = whnf_core(unfold_names(s_n, d_t->get_weight() + 1));
+            } else {
+                lean_assert(d_t && d_s && d_t->get_weight() == d_s->get_weight());
+                if (is_app(t_n) && is_app(s_n) && is_eqp(*d_t, *d_s)) {
+                    // try backtracking trick to avoild delta-reduction
+                    // TODO(Leo)
+                }
+                t_n = whnf_core(unfold_names(t_n, d_t->get_weight() - 1));
+                s_n = whnf_core(unfold_names(s_n, d_s->get_weight() - 1));
+            }
+            r = quick_is_conv(t_n, s_n, def_eq);
+            if (r != l_undef) return r == l_true;
+        }
+
+        if (m_env.proof_irrel()) {
+            // Proof irrelevance support
+            flet<bool> disable_cnstrs(m_cnstrs_enabled, false); // disable constraint generation
+            auto t_type = infer_type(t);
+            if (t_type && is_proposition(*t_type)) {
+                auto s_type = infer_type(s);
+                if (s_type)
+                    return is_def_eq(*t_type, *s_type);
+            }
+        }
+
+        if (m_env.eta()) {
+            lean_assert(!is_lambda(t) || !is_lambda(s));
+            // Eta-reduction support
+            if ((is_lambda(t) && try_eta(t, s)) ||
+                (is_lambda(s) && try_eta(s, t)))
+                return true;
+        }
+
+        return false;
+    }
+
+    /** \brief Return true iff t and s are definitionally equal */
+    bool is_def_eq(expr const & t, expr const & s) {
+        return is_conv(t, s, true);
+    }
+
+    bool is_proposition(expr const &) {
+        // TODO(Leo)
+        return false;
+    }
+
+    optional<expr> infer_type(expr const &) {
+        // TODO(Leo)
+        return none_expr();
+    }
 };
 }
diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h
index 118c0ad05..0aa2d6073 100644
--- a/src/kernel/type_checker.h
+++ b/src/kernel/type_checker.h
@@ -16,7 +16,7 @@ namespace lean {
 class constraint_handler {
 public:
     virtual ~constraint_handler();
-    void add_constr(constraint const & c);
+    void add_cnstr(constraint const & c);
 };
 
 /**