diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt
index ce27e69088..d23cba946a 100644
--- a/src/kernel/CMakeLists.txt
+++ b/src/kernel/CMakeLists.txt
@@ -1,6 +1,6 @@
 add_library(kernel OBJECT level.cpp expr.cpp expr_eq_fn.cpp for_each_fn.cpp
 replace_fn.cpp free_vars.cpp abstract.cpp instantiate.cpp
 formatter.cpp declaration.cpp environment.cpp pos_info_provider.cpp
-converter.cpp type_checker.cpp error_msgs.cpp kernel_exception.cpp
+type_checker.cpp error_msgs.cpp kernel_exception.cpp
 normalizer_extension.cpp init_module.cpp expr_cache.cpp
-default_converter.cpp equiv_manager.cpp abstract_type_context.cpp)
+equiv_manager.cpp abstract_type_context.cpp)
diff --git a/src/kernel/converter.cpp b/src/kernel/converter.cpp
deleted file mode 100644
index c23824dde3..0000000000
--- a/src/kernel/converter.cpp
+++ /dev/null
@@ -1,41 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-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 "kernel/converter.h"
-#include "kernel/expr_maps.h"
-#include "kernel/instantiate.h"
-#include "kernel/free_vars.h"
-#include "kernel/type_checker.h"
-#include "kernel/default_converter.h"
-
-namespace lean {
-expr converter::infer_type(type_checker & tc, expr const & e) { return tc.infer_type(e); }
-
-/** \brief Do nothing converter */
-struct dummy_converter : public converter {
-    virtual expr whnf(expr const & e, type_checker &) {
-        return e;
-    }
-    virtual bool is_def_eq(expr const &, expr const &, type_checker &) {
-        return true;
-    }
-    virtual bool is_opaque(declaration const &) const { return false; }
-    virtual optional<declaration> is_delta(expr const &) const { return optional<declaration>(); }
-    virtual optional<expr> is_stuck(expr const &, type_checker &) { return none_expr(); }
-};
-
-std::unique_ptr<converter> mk_dummy_converter() {
-    return std::unique_ptr<converter>(new dummy_converter());
-}
-
-void initialize_converter() {
-}
-
-void finalize_converter() {
-}
-}
diff --git a/src/kernel/converter.h b/src/kernel/converter.h
deleted file mode 100644
index 9b0be4535a..0000000000
--- a/src/kernel/converter.h
+++ /dev/null
@@ -1,40 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include <functional>
-#include "kernel/environment.h"
-
-namespace lean {
-class type_checker;
-
-class converter {
-protected:
-    expr infer_type(type_checker & tc, expr const & e);
-public:
-    virtual ~converter() {}
-    virtual bool is_opaque(declaration const & d) const = 0;
-    virtual optional<declaration> is_delta(expr const & e) const = 0;
-
-    virtual optional<expr> is_stuck(expr const & e, type_checker & c) = 0;
-    virtual expr whnf(expr const & e, type_checker & c) = 0;
-    virtual bool is_def_eq(expr const & t, expr const & s, type_checker & c) = 0;
-};
-
-/** \brief Converter that allows us to specify constants that should be considered opaque */
-template<typename Converter>
-class hint_converter : public Converter {
-    name_predicate m_pred;
-public:
-    hint_converter(environment const & env, name_predicate const & p):Converter(env), m_pred(p) {}
-    virtual bool is_opaque(declaration const & d) const { return m_pred(d.get_name()) || Converter::is_opaque(d); }
-};
-
-std::unique_ptr<converter> mk_dummy_converter();
-
-void initialize_converter();
-void finalize_converter();
-}
diff --git a/src/kernel/default_converter.cpp b/src/kernel/default_converter.cpp
deleted file mode 100644
index a2f5c7cc0a..0000000000
--- a/src/kernel/default_converter.cpp
+++ /dev/null
@@ -1,564 +0,0 @@
-/*
-Copyright (c) 2014-2015 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "util/interrupt.h"
-#include "util/flet.h"
-#include "util/fresh_name.h"
-#include "kernel/default_converter.h"
-#include "kernel/instantiate.h"
-#include "kernel/free_vars.h"
-#include "kernel/type_checker.h"
-#include "kernel/error_msgs.h"
-#include "library/metavar.h"
-#include "library/constraint.h"
-
-namespace lean {
-static expr * g_dont_care = nullptr;
-
-default_converter::default_converter(environment const & env, bool memoize):
-    m_env(env), m_memoize(memoize) {
-    m_tc  = nullptr;
-    m_jst = nullptr;
-}
-
-optional<expr> default_converter::expand_macro(expr const & m) {
-    lean_assert(is_macro(m));
-    return macro_def(m).expand(m, *m_tc);
-}
-
-/** \brief Apply normalizer extensions to \c e. */
-optional<expr> default_converter::norm_ext(expr const & e) {
-    return m_env.norm_ext()(e, *m_tc);
-}
-
-/** \brief Return true if \c e may be reduced later after metavariables are instantiated. */
-bool default_converter::is_stuck(expr const & e) {
-    return static_cast<bool>(m_env.norm_ext().is_stuck(e, *m_tc));
-}
-
-optional<expr> default_converter::is_stuck(expr const & e, type_checker & c) {
-    if (is_meta(e)) {
-        return some_expr(e);
-    } else {
-        return m_env.norm_ext().is_stuck(e, c);
-    }
-}
-
-/** \brief Weak head normal form core procedure. It does not perform delta reduction nor normalization extensions. */
-expr default_converter::whnf_core(expr const & e) {
-    check_system("whnf");
-
-    // handle easy cases
-    switch (e.kind()) {
-    case expr_kind::Var:  case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local:
-    case expr_kind::Pi:   case expr_kind::Constant: case expr_kind::Lambda:
-        return e;
-    case expr_kind::Macro: case expr_kind::App: case expr_kind::Let:
-        break;
-    }
-
-    // check cache
-    if (m_memoize) {
-        auto it = m_whnf_core_cache.find(e);
-        if (it != m_whnf_core_cache.end())
-            return it->second;
-    }
-
-    // do the actual work
-    expr r;
-    switch (e.kind()) {
-    case expr_kind::Var:  case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local:
-    case expr_kind::Pi:   case expr_kind::Constant: case expr_kind::Lambda:
-        lean_unreachable(); // LCOV_EXCL_LINE
-    case expr_kind::Macro:
-        if (auto m = expand_macro(e))
-            r = whnf_core(*m);
-        else
-            r = e;
-        break;
-    case expr_kind::App: {
-        buffer<expr> args;
-        expr f0 = get_app_rev_args(e, args);
-        expr f = whnf_core(f0);
-        if (is_lambda(f)) {
-            unsigned m = 1;
-            unsigned num_args = args.size();
-            while (is_lambda(binding_body(f)) && m < num_args) {
-                f = binding_body(f);
-                m++;
-            }
-            lean_assert(m <= num_args);
-            r = whnf_core(mk_rev_app(instantiate(binding_body(f), m, args.data() + (num_args - m)), num_args - m, args.data()));
-        } else {
-            r = f == f0 ? e : whnf_core(mk_rev_app(f, args.size(), args.data()));
-        }
-        break;
-    }
-    case expr_kind::Let:
-        r = whnf_core(instantiate(let_body(e), let_value(e)));
-        break;
-    }
-
-    if (m_memoize)
-        m_whnf_core_cache.insert(mk_pair(e, r));
-    return r;
-}
-
-bool default_converter::is_opaque(declaration const &) const {
-    return false;
-}
-
-/** \brief Expand \c e if it is non-opaque constant with height >= h */
-expr default_converter::unfold_name_core(expr e, unsigned h) {
-    if (is_constant(e)) {
-        if (auto d = m_env.find(const_name(e))) {
-            if (d->is_definition() && !is_opaque(*d) && d->get_height() >= h &&
-                length(const_levels(e)) == d->get_num_univ_params())
-                return unfold_name_core(instantiate_value_univ_params(*d, const_levels(e)), h);
-        }
-    }
-    return e;
-}
-
-/**
-   \brief Expand constants and application where the function is a constant.
-
-   The unfolding is only performend if the constant corresponds to
-   a non-opaque definition with height >= h.
-*/
-expr default_converter::unfold_names(expr const & e, unsigned h) {
-    if (is_app(e)) {
-        expr f0 = get_app_fn(e);
-        expr f  = unfold_name_core(f0, h);
-        if (is_eqp(f, f0)) {
-            return e;
-        } else {
-            buffer<expr> args;
-            get_app_rev_args(e, args);
-            return mk_rev_app(f, args);
-        }
-    } else {
-        return unfold_name_core(e, h);
-    }
-}
-
-/**
-   \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<declaration> default_converter::is_delta(expr const & e) const {
-    expr const & f = get_app_fn(e);
-    if (is_constant(f)) {
-        if (auto d = m_env.find(const_name(f)))
-            if (d->is_definition() && !is_opaque(*d))
-                return d;
-    }
-    return none_declaration();
-}
-
-/**
-   \brief Weak head normal form core procedure that perform delta reduction for non-opaque constants with
-   height greater than or equal to \c h.
-
-   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 default_converter::whnf_core(expr e, unsigned h) {
-    while (true) {
-        expr new_e = unfold_names(whnf_core(e), h);
-        if (is_eqp(e, new_e))
-            return e;
-        e = new_e;
-    }
-}
-
-/** \brief Put expression \c t in weak head normal form */
-expr default_converter::whnf(expr const & e_prime) {
-    // Do not cache easy cases
-    switch (e_prime.kind()) {
-    case expr_kind::Var: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local: case expr_kind::Pi:
-        return e_prime;
-    case expr_kind::Lambda:   case expr_kind::Macro: case expr_kind::App:
-    case expr_kind::Constant: case expr_kind::Let:
-        break;
-    }
-
-    expr e = e_prime;
-    // check cache
-    if (m_memoize) {
-        auto it = m_whnf_cache.find(e);
-        if (it != m_whnf_cache.end())
-            return it->second;
-    }
-
-    expr t = e;
-    while (true) {
-        expr t1 = whnf_core(t, 0);
-        if (auto new_t = norm_ext(t1)) {
-            t  = *new_t;
-        } else {
-            auto r = t1;
-            if (m_memoize)
-                m_whnf_cache.insert(mk_pair(e, r));
-            return r;
-        }
-    }
-}
-
-/**
-   \brief Given lambda/Pi expressions \c t and \c s, return true iff \c t is def eq to \c s.
-
-        t and s are definitionally equal
-           iff
-        domain(t) is definitionally equal to domain(s)
-        and
-        body(t) is definitionally equal to body(s)
-*/
-bool default_converter::is_def_eq_binding(expr t, expr s) {
-    lean_assert(t.kind() == s.kind());
-    lean_assert(is_binding(t));
-    expr_kind k = t.kind();
-    buffer<expr> subst;
-    do {
-        optional<expr> var_s_type;
-        if (binding_domain(t) != binding_domain(s)) {
-            var_s_type = instantiate_rev(binding_domain(s), subst.size(), subst.data());
-            expr var_t_type = instantiate_rev(binding_domain(t), subst.size(), subst.data());
-            if (!is_def_eq(var_t_type, *var_s_type))
-                return false;
-        }
-        if (!closed(binding_body(t)) || !closed(binding_body(s))) {
-            // local is used inside t or s
-            if (!var_s_type)
-                var_s_type = instantiate_rev(binding_domain(s), subst.size(), subst.data());
-            subst.push_back(mk_local(mk_fresh_name(), binding_name(s), *var_s_type, binding_info(s)));
-        } else {
-            subst.push_back(*g_dont_care); // don't care
-        }
-        t = binding_body(t);
-        s = binding_body(s);
-    } while (t.kind() == k && s.kind() == k);
-    return is_def_eq(instantiate_rev(t, subst.size(), subst.data()),
-                     instantiate_rev(s, subst.size(), subst.data()));
-}
-
-bool default_converter::is_def_eq(level const & l1, level const & l2) {
-    if (is_equivalent(l1, l2)) {
-        return true;
-    } else {
-        return false;
-    }
-}
-
-bool default_converter::is_def_eq(levels const & ls1, levels const & ls2) {
-    if (is_nil(ls1) && is_nil(ls2)) {
-        return true;
-    } else if (!is_nil(ls1) && !is_nil(ls2)) {
-        return
-            is_def_eq(head(ls1), head(ls2)) &&
-            is_def_eq(tail(ls1), tail(ls2));
-    } else {
-        return false;
-    }
-}
-
-/** \brief This is an auxiliary method for is_def_eq. It handles the "easy cases". */
-lbool default_converter::quick_is_def_eq(expr const & t, expr const & s, bool use_hash) {
-    if (m_eqv_manager.is_equiv(t, s, use_hash))
-        return l_true;
-    if (t.kind() == s.kind()) {
-        switch (t.kind()) {
-        case expr_kind::Lambda: case expr_kind::Pi:
-            return to_lbool(is_def_eq_binding(t, s));
-        case expr_kind::Sort:
-            return to_lbool(is_def_eq(sort_level(t), sort_level(s)));
-        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"
-}
-
-/**
-   \brief Return true if arguments of \c t are definitionally equal to arguments of \c s.
-   This method is used to implement an optimization in the method \c is_def_eq.
-*/
-bool default_converter::is_def_eq_args(expr t, expr s) {
-    while (is_app(t) && is_app(s)) {
-        if (!is_def_eq(app_arg(t), app_arg(s)))
-            return false;
-        t = app_fn(t);
-        s = app_fn(s);
-    }
-    return !is_app(t) && !is_app(s);
-}
-
-/** \brief Try to solve (fun (x : A), B) =?= s by trying eta-expansion on s */
-bool default_converter::try_eta_expansion_core(expr const & t, expr const & s) {
-    if (is_lambda(t) && !is_lambda(s)) {
-        expr s_type = whnf(infer_type(s));
-        constraint_seq aux_cs;
-        if (!is_pi(s_type))
-            return false;
-        expr new_s  = mk_lambda(binding_name(s_type), binding_domain(s_type), mk_app(s, Var(0)), binding_info(s_type));
-        if (!is_def_eq(t, new_s))
-            return false;
-        return true;
-    } else {
-        return false;
-    }
-}
-
-/** \brief Return true if \c t and \c s are definitionally equal because they are applications of the form
-    <tt>(f a_1 ... a_n)</tt> <tt>(g b_1 ... b_n)</tt>, and \c f and \c g are definitionally equal, and
-    \c a_i and \c b_i are also definitionally equal for every 1 <= i <= n.
-    Return false otherwise.
-*/
-bool default_converter::is_def_eq_app(expr const & t, expr const & s) {
-    if (is_app(t) && is_app(s)) {
-        buffer<expr> t_args;
-        buffer<expr> s_args;
-        expr t_fn = get_app_args(t, t_args);
-        expr s_fn = get_app_args(s, s_args);
-        if (is_def_eq(t_fn, s_fn) && t_args.size() == s_args.size()) {
-            unsigned i = 0;
-            for (; i < t_args.size(); i++) {
-                if (!is_def_eq(t_args[i], s_args[i]))
-                    break;
-            }
-            if (i == t_args.size())
-                return true;
-        }
-    }
-    return false;
-}
-
-/** \brief remark: is_prop returns true only if \c e is reducible to Prop.
-*/
-bool default_converter::is_prop(expr const & e) {
-    return whnf(infer_type(e)) == mk_Prop();
-}
-
-/** \brief Return true if \c t and \c s are definitionally equal due to proof irrelevant.
-    Return false otherwise.
-*/
-bool default_converter::is_def_eq_proof_irrel(expr const & t, expr const & s) {
-    if (!m_env.prop_proof_irrel())
-        return false;
-    // Proof irrelevance support for Prop (aka Type.{0})
-    expr t_type = infer_type(t);
-    expr s_type = infer_type(s);
-    return is_prop(t_type) && is_def_eq(t_type, s_type);
-}
-
-bool default_converter::failed_before(expr const & t, expr const & s) const {
-    if (t.hash() < s.hash()) {
-        return m_failure_cache.find(mk_pair(t, s)) != m_failure_cache.end();
-    } else if (t.hash() > s.hash()) {
-        return m_failure_cache.find(mk_pair(s, t)) != m_failure_cache.end();
-    } else {
-        return
-            m_failure_cache.find(mk_pair(t, s)) != m_failure_cache.end() ||
-            m_failure_cache.find(mk_pair(s, t)) != m_failure_cache.end();
-    }
-}
-
-void default_converter::cache_failure(expr const & t, expr const & s) {
-    if (t.hash() <= s.hash())
-        m_failure_cache.insert(mk_pair(t, s));
-    else
-        m_failure_cache.insert(mk_pair(s, t));
-}
-
-/**
-   \brief Perform one lazy delta-reduction step.
-   Return
-   - l_true if t_n and s_n are definitionally equal.
-   - l_false if they are not definitionally equal.
-   - l_undef it the step did not manage to establish whether they are definitionally equal or not.
-
-   \remark t_n, s_n and cs are updated.
-*/
-auto default_converter::lazy_delta_reduction_step(expr & t_n, expr & s_n) -> reduction_status {
-    auto d_t = is_delta(t_n);
-    auto d_s = is_delta(s_n);
-    if (!d_t && !d_s) {
-        return reduction_status::DefUnknown;
-    } 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->is_theorem() && d_s->is_theorem()) {
-        t_n = whnf_core(unfold_names(t_n, d_t->get_height()));
-    } else if (!d_s->is_theorem() && d_t->is_theorem()) {
-        s_n = whnf_core(unfold_names(s_n, d_s->get_height()));
-    } else if (!d_t->is_theorem() && d_t->get_height() > d_s->get_height()) {
-        t_n = whnf_core(unfold_names(t_n, d_s->get_height() + 1));
-    } else if (!d_s->is_theorem() && d_t->get_height() < d_s->get_height()) {
-        s_n = whnf_core(unfold_names(s_n, d_t->get_height() + 1));
-    } else {
-        if (is_app(t_n) && is_app(s_n) && is_eqp(*d_t, *d_s)) {
-            // If t_n and s_n are both applications of the same (non-opaque) definition,
-            if (has_expr_metavar(t_n) || has_expr_metavar(s_n)) {
-                // We let the unifier deal with cases such as
-                // (f ...) =?= (f ...)
-                // when t_n or s_n contains metavariables
-                return reduction_status::DefUnknown;
-            } else {
-                // Optimization:
-                // We try to check if their arguments are definitionally equal.
-                // If they are, then t_n and s_n must be definitionally equal, and we can
-                // skip the delta-reduction step.
-                // If the flag use_conv_opt() is not true, then we skip this optimization
-                if (!is_opaque(*d_t) && d_t->use_conv_opt() && !failed_before(t_n, s_n)) {
-                    if (is_def_eq(const_levels(get_app_fn(t_n)), const_levels(get_app_fn(s_n))) &&
-                        is_def_eq_args(t_n, s_n)) {
-                        return reduction_status::DefEqual;
-                    } else {
-                        cache_failure(t_n, s_n);
-                    }
-                }
-            }
-        }
-        t_n = whnf_core(unfold_names(t_n, d_t->get_height() - 1));
-        s_n = whnf_core(unfold_names(s_n, d_s->get_height() - 1));
-    }
-    switch (quick_is_def_eq(t_n, s_n)) {
-    case l_true:  return reduction_status::DefEqual;
-    case l_false: return reduction_status::DefDiff;
-    case l_undef: return reduction_status::Continue;
-    }
-    lean_unreachable();
-}
-
-lbool default_converter::lazy_delta_reduction(expr & t_n, expr & s_n) {
-    while (true) {
-        switch (lazy_delta_reduction_step(t_n, s_n)) {
-        case reduction_status::Continue:   break;
-        case reduction_status::DefUnknown: return l_undef;
-        case reduction_status::DefEqual:   return l_true;
-        case reduction_status::DefDiff:    return l_false;
-        }
-    }
-}
-
-auto default_converter::ext_reduction_step(expr & t_n, expr & s_n) -> reduction_status {
-    auto new_t_n = norm_ext(t_n);
-    auto new_s_n = norm_ext(s_n);
-    if (!new_t_n && !new_s_n)
-        return reduction_status::DefUnknown;
-    if (new_t_n)
-        t_n = whnf_core(*new_t_n);
-    if (new_s_n)
-        s_n = whnf_core(*new_s_n);
-    switch (quick_is_def_eq(t_n, s_n)) {
-    case l_true:  return reduction_status::DefEqual;
-    case l_false: return reduction_status::DefDiff;
-    case l_undef: return reduction_status::Continue;
-    }
-    lean_unreachable();
-}
-
-// Apply lazy delta-reduction and then normalizer extensions
-lbool default_converter::reduce_def_eq(expr & t_n, expr & s_n) {
-    while (true) {
-        // first, keep applying lazy delta-reduction while applicable
-        lbool r = lazy_delta_reduction(t_n, s_n);
-        if (r != l_undef) return r;
-
-        // try normalizer extensions
-        switch (ext_reduction_step(t_n, s_n)) {
-        case reduction_status::Continue:   break;
-        case reduction_status::DefUnknown: return l_undef;
-        case reduction_status::DefEqual:   return l_true;
-        case reduction_status::DefDiff:    return l_false;
-        }
-    }
-}
-
-bool default_converter::postpone_is_def_eq(expr const & t, expr const & s) {
-    if (has_expr_metavar(t) || has_expr_metavar(s)) {
-        optional<declaration> d_t = is_delta(t);
-        optional<declaration> d_s = is_delta(s);
-        if (d_t && d_s && is_eqp(*d_t, *d_s))
-            return true;
-        else if (is_stuck(t) && is_stuck(s))
-            return true;
-    }
-    return false;
-}
-
-bool default_converter::is_def_eq_core(expr const & t, expr const & s) {
-    check_system("is_definitionally_equal");
-    bool use_hash = true;
-    lbool r = quick_is_def_eq(t, s, use_hash);
-    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_def_eq(t_n, s_n);
-        if (r != l_undef) return r == l_true;
-    }
-
-    r = reduce_def_eq(t_n, s_n);
-    if (r != l_undef) return r == l_true;
-
-    if (is_constant(t_n) && is_constant(s_n) && const_name(t_n) == const_name(s_n) &&
-        is_def_eq(const_levels(t_n), const_levels(s_n)))
-        return true;
-
-    if (is_local(t_n) && is_local(s_n) && mlocal_name(t_n) == mlocal_name(s_n))
-        return true;
-
-    bool postpone = postpone_is_def_eq(t_n, s_n);
-
-    // At this point, t_n and s_n are in weak head normal form (modulo meta-variables and proof irrelevance)
-    if (!postpone && is_def_eq_app(t_n, s_n))
-        return true;
-
-    if (try_eta_expansion(t_n, s_n))
-        return true;
-
-    if (is_def_eq_proof_irrel(t, s))
-        return true;
-
-    return false;
-}
-
-bool default_converter::is_def_eq(expr const & t, expr const & s) {
-    bool r = is_def_eq_core(t, s);
-    if (r)
-        m_eqv_manager.add_equiv(t, s);
-    return r;
-}
-
-/** Return true iff t is definitionally equal to s. */
-bool default_converter::is_def_eq(expr const & t, expr const & s, type_checker & c) {
-    flet<type_checker*>          set_tc(m_tc, &c);
-    return is_def_eq(t, s);
-}
-
-expr default_converter::whnf(expr const & e, type_checker & c) {
-    flet<type_checker*>          set_tc(m_tc, &c);
-    return whnf(e);
-}
-
-void initialize_default_converter() {
-    g_dont_care = new expr(Const("dontcare"));
-}
-
-void finalize_default_converter() {
-    delete g_dont_care;
-}
-}
diff --git a/src/kernel/default_converter.h b/src/kernel/default_converter.h
deleted file mode 100644
index c881672f62..0000000000
--- a/src/kernel/default_converter.h
+++ /dev/null
@@ -1,86 +0,0 @@
-/*
-Copyright (c) 2014-2015 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include <unordered_set>
-#include "util/lbool.h"
-#include "kernel/environment.h"
-#include "kernel/converter.h"
-#include "kernel/expr_maps.h"
-#include "kernel/equiv_manager.h"
-#include "kernel/expr_pair.h"
-#include "library/justification.h"
-
-namespace lean {
-/** \brief Converter used in the kernel */
-class default_converter : public converter {
-protected:
-    typedef std::unordered_set<expr_pair, expr_pair_hash, expr_pair_eq> expr_pair_set;
-    environment             m_env;
-    bool                    m_memoize;
-    expr_struct_map<expr>   m_whnf_core_cache;
-    expr_struct_map<expr>   m_whnf_cache;
-    equiv_manager           m_eqv_manager;
-    expr_pair_set           m_failure_cache;
-
-    // The two auxiliary fields are set when the public methods whnf and is_def_eq are invoked.
-    // The goal is to avoid to keep carrying them around.
-    type_checker *                              m_tc;
-    delayed_justification *                     m_jst;
-
-    virtual bool is_stuck(expr const & e);
-    virtual optional<expr> norm_ext(expr const & e);
-
-    expr infer_type(expr const & e) { return converter::infer_type(*m_tc, e); }
-    optional<expr> expand_macro(expr const & m);
-    expr whnf_core(expr const & e);
-    expr unfold_name_core(expr e, unsigned w);
-    expr unfold_names(expr const & e, unsigned w);
-    expr whnf_core(expr e, unsigned w);
-
-    expr whnf(expr const & e_prime);
-
-    bool is_def_eq_binding(expr t, expr s);
-    bool is_def_eq(level const & l1, level const & l2);
-    bool is_def_eq(levels const & ls1, levels const & ls2);
-
-    lbool quick_is_def_eq(expr const & t, expr const & s, bool use_hash = false);
-    bool is_def_eq_args(expr t, expr s);
-    bool try_eta_expansion_core(expr const & t, expr const & s);
-    bool try_eta_expansion(expr const & t, expr const & s) {
-        return try_eta_expansion_core(t, s) || try_eta_expansion_core(s, t);
-    }
-    bool is_def_eq(expr const & t, expr const & s);
-    bool is_def_eq_app(expr const & t, expr const & s);
-    bool is_def_eq_proof_irrel(expr const & t, expr const & s);
-
-    bool failed_before(expr const & t, expr const & s) const;
-    void cache_failure(expr const & t, expr const & s);
-
-    bool is_prop(expr const & e);
-
-    bool is_def_eq_core(expr const & t, expr const & s);
-
-    enum class reduction_status { Continue, DefUnknown, DefEqual, DefDiff };
-    reduction_status lazy_delta_reduction_step(expr & t_n, expr & s_n);
-    lbool lazy_delta_reduction(expr & t_n, expr & s_n);
-    reduction_status ext_reduction_step(expr & t_n, expr & s_n);
-    virtual lbool reduce_def_eq(expr & t_n, expr & s_n);
-    virtual bool postpone_is_def_eq(expr const & t, expr const & s);
-public:
-    default_converter(environment const & env, bool memoize = true);
-
-    virtual optional<declaration> is_delta(expr const & e) const;
-    virtual bool is_opaque(declaration const & d) const;
-
-    virtual optional<expr> is_stuck(expr const & e, type_checker & c);
-    virtual expr whnf(expr const & e_prime, type_checker & c);
-    virtual bool is_def_eq(expr const & t, expr const & s, type_checker & c);
-};
-
-void initialize_default_converter();
-void finalize_default_converter();
-}
diff --git a/src/kernel/environment.h b/src/kernel/environment.h
index 9d2c6bc5a2..c4bac1204f 100644
--- a/src/kernel/environment.h
+++ b/src/kernel/environment.h
@@ -229,8 +229,7 @@ class name_generator;
    Only the type_checker class can create certified declarations.
 */
 class certified_declaration {
-    friend certified_declaration check(environment const & env, declaration const & d,
-                                       name_predicate const & opaque_hints);
+    friend certified_declaration check(environment const & env, declaration const & d);
     environment_id m_id;
     declaration    m_declaration;
     certified_declaration(environment_id const & id, declaration const & d):m_id(id), m_declaration(d) {}
diff --git a/src/kernel/init_module.cpp b/src/kernel/init_module.cpp
index cbfd9db526..d2014b1cb9 100644
--- a/src/kernel/init_module.cpp
+++ b/src/kernel/init_module.cpp
@@ -5,21 +5,17 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "kernel/environment.h"
-#include "kernel/converter.h"
 #include "kernel/type_checker.h"
 #include "kernel/expr.h"
 #include "kernel/formatter.h"
 #include "kernel/level.h"
 #include "kernel/declaration.h"
-#include "kernel/default_converter.h"
 
 namespace lean {
 void initialize_kernel_module() {
     initialize_level();
     initialize_expr();
     initialize_declaration();
-    initialize_default_converter();
-    initialize_converter();
     initialize_type_checker();
     initialize_environment();
     initialize_formatter();
@@ -28,8 +24,6 @@ void finalize_kernel_module() {
     finalize_formatter();
     finalize_environment();
     finalize_type_checker();
-    finalize_converter();
-    finalize_default_converter();
     finalize_declaration();
     finalize_expr();
     finalize_level();
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index 9b1c6209f6..f5ee746c0d 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -13,7 +13,6 @@ Author: Leonardo de Moura
 #include "util/scoped_map.h"
 #include "util/fresh_name.h"
 #include "kernel/type_checker.h"
-#include "kernel/default_converter.h"
 #include "kernel/expr_maps.h"
 #include "kernel/instantiate.h"
 #include "kernel/free_vars.h"
@@ -23,27 +22,25 @@ Author: Leonardo de Moura
 #include "kernel/replace_fn.h"
 
 namespace lean {
+static expr * g_dont_care = nullptr;
+
 optional<expr> type_checker::expand_macro(expr const & m) {
     lean_assert(is_macro(m));
     return macro_def(m).expand(m, *this);
 }
 
-/**
-   \brief Return the body of the given binder, where the free variable #0 is replaced with a fresh local constant.
-   It also returns the fresh local constant.
-*/
+/** \brief Return the body of the given binder, where the free variable #0 is replaced with a fresh local constant.
+    It also returns the fresh local constant. */
 pair<expr, expr> type_checker::open_binding_body(expr const & e) {
     expr local     = mk_local(mk_fresh_name(), binding_name(e), binding_domain(e), binding_info(e));
     return mk_pair(instantiate(binding_body(e), local), local);
 }
 
-/**
-   \brief Make sure \c e "is" a sort, and return the corresponding sort.
-   If \c e is not a sort, then the whnf procedure is invoked.
+/** \brief Make sure \c e "is" a sort, and return the corresponding sort.
+    If \c e is not a sort, then the whnf procedure is invoked.
 
-   \remark \c s is used to extract position (line number information) when an
-   error message is produced
-*/
+    \remark \c s is used to extract position (line number information) when an
+    error message is produced */
 expr type_checker::ensure_sort_core(expr e, expr const & s) {
     if (is_sort(e))
         return e;
@@ -198,11 +195,8 @@ expr type_checker::infer_let(expr const & e, bool infer_only) {
     return infer_type_core(instantiate(let_body(e), let_value(e)), infer_only);
 }
 
-/**
-   \brief Return type of expression \c e, if \c infer_only is false, then it also check whether \c e is type correct or not.
-
-   \pre closed(e)
-*/
+/** \brief Return type of expression \c e, if \c infer_only is false, then it also check whether \c e is type correct or not.
+    \pre closed(e) */
 expr type_checker::infer_type_core(expr const & e, bool infer_only) {
     if (is_var(e))
         throw_kernel_exception(m_env, "type checker does not support free variables, replace them with local constants before invoking it", e);
@@ -260,14 +254,10 @@ expr type_checker::ensure_pi(expr const & e, expr const & s) {
     return ensure_pi_core(e, s);
 }
 
-bool type_checker::is_def_eq(expr const & t, expr const & s) {
-    return m_conv->is_def_eq(t, s, *this);
-}
-
 bool type_checker::is_def_eq_types(expr const & t, expr const & s) {
     expr t1 = infer_type_core(t, true);
     expr t2 = infer_type_core(s, true);
-    return m_conv->is_def_eq(t1, t2, *this);
+    return is_def_eq(t1, t2);
 }
 
 /** \brief Return true iff \c e is a proposition */
@@ -275,36 +265,483 @@ bool type_checker::is_prop(expr const & e) {
     return m_env.impredicative() && whnf(infer_type(e)) == mk_Prop();
 }
 
-expr type_checker::whnf(expr const & t) {
-    return m_conv->whnf(t, *this);
+/** \brief Apply normalizer extensions to \c e. */
+optional<expr> type_checker::norm_ext(expr const & e) {
+    return m_env.norm_ext()(e, *this);
 }
 
-bool type_checker::is_opaque(declaration const & d) const {
-    return m_conv->is_opaque(d);
+/** \brief Return true if \c e may be reduced later after metavariables are instantiated. */
+optional<expr> type_checker::is_stuck(expr const & e) {
+    if (is_meta(e)) {
+        return some_expr(e);
+    } else {
+        return m_env.norm_ext().is_stuck(e, *this);
+    }
 }
 
-bool type_checker::is_opaque(expr const & c) const {
-    lean_assert(is_constant(c));
-    if (auto d = m_env.find(const_name(c)))
-        return d->is_definition() && is_opaque(*d);
-    else
+/** \brief Weak head normal form core procedure. It does not perform delta reduction nor normalization extensions. */
+expr type_checker::whnf_core(expr const & e) {
+    check_system("whnf");
+
+    // handle easy cases
+    switch (e.kind()) {
+    case expr_kind::Var:  case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local:
+    case expr_kind::Pi:   case expr_kind::Constant: case expr_kind::Lambda:
+        return e;
+    case expr_kind::Macro: case expr_kind::App: case expr_kind::Let:
+        break;
+    }
+
+    // check cache
+    if (m_memoize) {
+        auto it = m_whnf_core_cache.find(e);
+        if (it != m_whnf_core_cache.end())
+            return it->second;
+    }
+
+    // do the actual work
+    expr r;
+    switch (e.kind()) {
+    case expr_kind::Var:  case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local:
+    case expr_kind::Pi:   case expr_kind::Constant: case expr_kind::Lambda:
+        lean_unreachable(); // LCOV_EXCL_LINE
+    case expr_kind::Macro:
+        if (auto m = expand_macro(e))
+            r = whnf_core(*m);
+        else
+            r = e;
+        break;
+    case expr_kind::App: {
+        buffer<expr> args;
+        expr f0 = get_app_rev_args(e, args);
+        expr f = whnf_core(f0);
+        if (is_lambda(f)) {
+            unsigned m = 1;
+            unsigned num_args = args.size();
+            while (is_lambda(binding_body(f)) && m < num_args) {
+                f = binding_body(f);
+                m++;
+            }
+            lean_assert(m <= num_args);
+            r = whnf_core(mk_rev_app(instantiate(binding_body(f), m, args.data() + (num_args - m)), num_args - m, args.data()));
+        } else {
+            r = f == f0 ? e : whnf_core(mk_rev_app(f, args.size(), args.data()));
+        }
+        break;
+    }
+    case expr_kind::Let:
+        r = whnf_core(instantiate(let_body(e), let_value(e)));
+        break;
+    }
+
+    if (m_memoize)
+        m_whnf_core_cache.insert(mk_pair(e, r));
+    return r;
+}
+
+/** \brief Expand \c e if it is non-opaque constant with height >= h */
+expr type_checker::unfold_name_core(expr e, unsigned h) {
+    if (is_constant(e)) {
+        if (auto d = m_env.find(const_name(e))) {
+            if (d->is_definition() && d->get_height() >= h &&
+                length(const_levels(e)) == d->get_num_univ_params())
+                return unfold_name_core(instantiate_value_univ_params(*d, const_levels(e)), h);
+        }
+    }
+    return e;
+}
+
+/** \brief Expand constants and application where the function is a constant.
+
+    The unfolding is only performend if the constant corresponds to
+    a non-opaque definition with height >= h. */
+expr type_checker::unfold_names(expr const & e, unsigned h) {
+    if (is_app(e)) {
+        expr f0 = get_app_fn(e);
+        expr f  = unfold_name_core(f0, h);
+        if (is_eqp(f, f0)) {
+            return e;
+        } else {
+            buffer<expr> args;
+            get_app_rev_args(e, args);
+            return mk_rev_app(f, args);
+        }
+    } else {
+        return unfold_name_core(e, h);
+    }
+}
+
+/** \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<declaration> type_checker::is_delta(expr const & e) const {
+    expr const & f = get_app_fn(e);
+    if (is_constant(f)) {
+        if (auto d = m_env.find(const_name(f)))
+            if (d->is_definition())
+                return d;
+    }
+    return none_declaration();
+}
+
+/** \brief Weak head normal form core procedure that perform delta reduction for non-opaque constants with
+    height greater than or equal to \c h.
+
+    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 type_checker::whnf_core(expr e, unsigned h) {
+    while (true) {
+        expr new_e = unfold_names(whnf_core(e), h);
+        if (is_eqp(e, new_e))
+            return e;
+        e = new_e;
+    }
+}
+
+/** \brief Put expression \c t in weak head normal form */
+expr type_checker::whnf(expr const & e_prime) {
+    // Do not cache easy cases
+    switch (e_prime.kind()) {
+    case expr_kind::Var: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local: case expr_kind::Pi:
+        return e_prime;
+    case expr_kind::Lambda:   case expr_kind::Macro: case expr_kind::App:
+    case expr_kind::Constant: case expr_kind::Let:
+        break;
+    }
+
+    expr e = e_prime;
+    // check cache
+    if (m_memoize) {
+        auto it = m_whnf_cache.find(e);
+        if (it != m_whnf_cache.end())
+            return it->second;
+    }
+
+    expr t = e;
+    while (true) {
+        expr t1 = whnf_core(t, 0);
+        if (auto new_t = norm_ext(t1)) {
+            t  = *new_t;
+        } else {
+            auto r = t1;
+            if (m_memoize)
+                m_whnf_cache.insert(mk_pair(e, r));
+            return r;
+        }
+    }
+}
+
+/** \brief Given lambda/Pi expressions \c t and \c s, return true iff \c t is def eq to \c s.
+
+        t and s are definitionally equal
+           iff
+        domain(t) is definitionally equal to domain(s)
+        and
+        body(t) is definitionally equal to body(s) */
+bool type_checker::is_def_eq_binding(expr t, expr s) {
+    lean_assert(t.kind() == s.kind());
+    lean_assert(is_binding(t));
+    expr_kind k = t.kind();
+    buffer<expr> subst;
+    do {
+        optional<expr> var_s_type;
+        if (binding_domain(t) != binding_domain(s)) {
+            var_s_type = instantiate_rev(binding_domain(s), subst.size(), subst.data());
+            expr var_t_type = instantiate_rev(binding_domain(t), subst.size(), subst.data());
+            if (!is_def_eq(var_t_type, *var_s_type))
+                return false;
+        }
+        if (!closed(binding_body(t)) || !closed(binding_body(s))) {
+            // local is used inside t or s
+            if (!var_s_type)
+                var_s_type = instantiate_rev(binding_domain(s), subst.size(), subst.data());
+            subst.push_back(mk_local(mk_fresh_name(), binding_name(s), *var_s_type, binding_info(s)));
+        } else {
+            subst.push_back(*g_dont_care); // don't care
+        }
+        t = binding_body(t);
+        s = binding_body(s);
+    } while (t.kind() == k && s.kind() == k);
+    return is_def_eq(instantiate_rev(t, subst.size(), subst.data()),
+                     instantiate_rev(s, subst.size(), subst.data()));
+}
+
+bool type_checker::is_def_eq(level const & l1, level const & l2) {
+    if (is_equivalent(l1, l2)) {
         return true;
+    } else {
+        return false;
+    }
 }
 
-type_checker::type_checker(environment const & env, std::unique_ptr<converter> && conv, bool memoize):
-    m_env(env), m_conv(std::move(conv)),
-    m_memoize(memoize), m_params(nullptr) {
+bool type_checker::is_def_eq(levels const & ls1, levels const & ls2) {
+    if (is_nil(ls1) && is_nil(ls2)) {
+        return true;
+    } else if (!is_nil(ls1) && !is_nil(ls2)) {
+        return
+            is_def_eq(head(ls1), head(ls2)) &&
+            is_def_eq(tail(ls1), tail(ls2));
+    } else {
+        return false;
+    }
+}
+
+/** \brief This is an auxiliary method for is_def_eq. It handles the "easy cases". */
+lbool type_checker::quick_is_def_eq(expr const & t, expr const & s, bool use_hash) {
+    if (m_eqv_manager.is_equiv(t, s, use_hash))
+        return l_true;
+    if (t.kind() == s.kind()) {
+        switch (t.kind()) {
+        case expr_kind::Lambda: case expr_kind::Pi:
+            return to_lbool(is_def_eq_binding(t, s));
+        case expr_kind::Sort:
+            return to_lbool(is_def_eq(sort_level(t), sort_level(s)));
+        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"
+}
+
+/** \brief Return true if arguments of \c t are definitionally equal to arguments of \c s.
+    This method is used to implement an optimization in the method \c is_def_eq. */
+bool type_checker::is_def_eq_args(expr t, expr s) {
+    while (is_app(t) && is_app(s)) {
+        if (!is_def_eq(app_arg(t), app_arg(s)))
+            return false;
+        t = app_fn(t);
+        s = app_fn(s);
+    }
+    return !is_app(t) && !is_app(s);
+}
+
+/** \brief Try to solve (fun (x : A), B) =?= s by trying eta-expansion on s */
+bool type_checker::try_eta_expansion_core(expr const & t, expr const & s) {
+    if (is_lambda(t) && !is_lambda(s)) {
+        expr s_type = whnf(infer_type(s));
+        if (!is_pi(s_type))
+            return false;
+        expr new_s  = mk_lambda(binding_name(s_type), binding_domain(s_type), mk_app(s, Var(0)), binding_info(s_type));
+        if (!is_def_eq(t, new_s))
+            return false;
+        return true;
+    } else {
+        return false;
+    }
+}
+
+/** \brief Return true if \c t and \c s are definitionally equal because they are applications of the form
+    <tt>(f a_1 ... a_n)</tt> <tt>(g b_1 ... b_n)</tt>, and \c f and \c g are definitionally equal, and
+    \c a_i and \c b_i are also definitionally equal for every 1 <= i <= n.
+    Return false otherwise. */
+bool type_checker::is_def_eq_app(expr const & t, expr const & s) {
+    if (is_app(t) && is_app(s)) {
+        buffer<expr> t_args;
+        buffer<expr> s_args;
+        expr t_fn = get_app_args(t, t_args);
+        expr s_fn = get_app_args(s, s_args);
+        if (is_def_eq(t_fn, s_fn) && t_args.size() == s_args.size()) {
+            unsigned i = 0;
+            for (; i < t_args.size(); i++) {
+                if (!is_def_eq(t_args[i], s_args[i]))
+                    break;
+            }
+            if (i == t_args.size())
+                return true;
+        }
+    }
+    return false;
+}
+
+/** \brief Return true if \c t and \c s are definitionally equal due to proof irrelevant.
+    Return false otherwise. */
+bool type_checker::is_def_eq_proof_irrel(expr const & t, expr const & s) {
+    if (!m_env.prop_proof_irrel())
+        return false;
+    // Proof irrelevance support for Prop (aka Type.{0})
+    expr t_type = infer_type(t);
+    expr s_type = infer_type(s);
+    return is_prop(t_type) && is_def_eq(t_type, s_type);
+}
+
+bool type_checker::failed_before(expr const & t, expr const & s) const {
+    if (t.hash() < s.hash()) {
+        return m_failure_cache.find(mk_pair(t, s)) != m_failure_cache.end();
+    } else if (t.hash() > s.hash()) {
+        return m_failure_cache.find(mk_pair(s, t)) != m_failure_cache.end();
+    } else {
+        return
+            m_failure_cache.find(mk_pair(t, s)) != m_failure_cache.end() ||
+            m_failure_cache.find(mk_pair(s, t)) != m_failure_cache.end();
+    }
+}
+
+void type_checker::cache_failure(expr const & t, expr const & s) {
+    if (t.hash() <= s.hash())
+        m_failure_cache.insert(mk_pair(t, s));
+    else
+        m_failure_cache.insert(mk_pair(s, t));
+}
+
+/** \brief Perform one lazy delta-reduction step.
+     Return
+     - l_true if t_n and s_n are definitionally equal.
+     - l_false if they are not definitionally equal.
+     - l_undef it the step did not manage to establish whether they are definitionally equal or not.
+
+     \remark t_n, s_n and cs are updated. */
+auto type_checker::lazy_delta_reduction_step(expr & t_n, expr & s_n) -> reduction_status {
+    auto d_t = is_delta(t_n);
+    auto d_s = is_delta(s_n);
+    if (!d_t && !d_s) {
+        return reduction_status::DefUnknown;
+    } 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->is_theorem() && d_s->is_theorem()) {
+        t_n = whnf_core(unfold_names(t_n, d_t->get_height()));
+    } else if (!d_s->is_theorem() && d_t->is_theorem()) {
+        s_n = whnf_core(unfold_names(s_n, d_s->get_height()));
+    } else if (!d_t->is_theorem() && d_t->get_height() > d_s->get_height()) {
+        t_n = whnf_core(unfold_names(t_n, d_s->get_height() + 1));
+    } else if (!d_s->is_theorem() && d_t->get_height() < d_s->get_height()) {
+        s_n = whnf_core(unfold_names(s_n, d_t->get_height() + 1));
+    } else {
+        if (is_app(t_n) && is_app(s_n) && is_eqp(*d_t, *d_s)) {
+            // If t_n and s_n are both applications of the same (non-opaque) definition,
+            if (has_expr_metavar(t_n) || has_expr_metavar(s_n)) {
+                // We let the unifier deal with cases such as
+                // (f ...) =?= (f ...)
+                // when t_n or s_n contains metavariables
+                return reduction_status::DefUnknown;
+            } else {
+                // Optimization:
+                // We try to check if their arguments are definitionally equal.
+                // If they are, then t_n and s_n must be definitionally equal, and we can
+                // skip the delta-reduction step.
+                // If the flag use_conv_opt() is not true, then we skip this optimization
+                if (d_t->use_conv_opt() && !failed_before(t_n, s_n)) {
+                    if (is_def_eq(const_levels(get_app_fn(t_n)), const_levels(get_app_fn(s_n))) &&
+                        is_def_eq_args(t_n, s_n)) {
+                        return reduction_status::DefEqual;
+                    } else {
+                        cache_failure(t_n, s_n);
+                    }
+                }
+            }
+        }
+        t_n = whnf_core(unfold_names(t_n, d_t->get_height() - 1));
+        s_n = whnf_core(unfold_names(s_n, d_s->get_height() - 1));
+    }
+    switch (quick_is_def_eq(t_n, s_n)) {
+    case l_true:  return reduction_status::DefEqual;
+    case l_false: return reduction_status::DefDiff;
+    case l_undef: return reduction_status::Continue;
+    }
+    lean_unreachable();
+}
+
+lbool type_checker::lazy_delta_reduction(expr & t_n, expr & s_n) {
+    while (true) {
+        switch (lazy_delta_reduction_step(t_n, s_n)) {
+        case reduction_status::Continue:   break;
+        case reduction_status::DefUnknown: return l_undef;
+        case reduction_status::DefEqual:   return l_true;
+        case reduction_status::DefDiff:    return l_false;
+        }
+    }
+}
+
+auto type_checker::ext_reduction_step(expr & t_n, expr & s_n) -> reduction_status {
+    auto new_t_n = norm_ext(t_n);
+    auto new_s_n = norm_ext(s_n);
+    if (!new_t_n && !new_s_n)
+        return reduction_status::DefUnknown;
+    if (new_t_n)
+        t_n = whnf_core(*new_t_n);
+    if (new_s_n)
+        s_n = whnf_core(*new_s_n);
+    switch (quick_is_def_eq(t_n, s_n)) {
+    case l_true:  return reduction_status::DefEqual;
+    case l_false: return reduction_status::DefDiff;
+    case l_undef: return reduction_status::Continue;
+    }
+    lean_unreachable();
+}
+
+// Apply lazy delta-reduction and then normalizer extensions
+lbool type_checker::reduce_def_eq(expr & t_n, expr & s_n) {
+    while (true) {
+        // first, keep applying lazy delta-reduction while applicable
+        lbool r = lazy_delta_reduction(t_n, s_n);
+        if (r != l_undef) return r;
+
+        // try normalizer extensions
+        switch (ext_reduction_step(t_n, s_n)) {
+        case reduction_status::Continue:   break;
+        case reduction_status::DefUnknown: return l_undef;
+        case reduction_status::DefEqual:   return l_true;
+        case reduction_status::DefDiff:    return l_false;
+        }
+    }
+}
+
+bool type_checker::is_def_eq_core(expr const & t, expr const & s) {
+    check_system("is_definitionally_equal");
+    bool use_hash = true;
+    lbool r = quick_is_def_eq(t, s, use_hash);
+    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_def_eq(t_n, s_n);
+        if (r != l_undef) return r == l_true;
+    }
+
+    r = reduce_def_eq(t_n, s_n);
+    if (r != l_undef) return r == l_true;
+
+    if (is_constant(t_n) && is_constant(s_n) && const_name(t_n) == const_name(s_n) &&
+        is_def_eq(const_levels(t_n), const_levels(s_n)))
+        return true;
+
+    if (is_local(t_n) && is_local(s_n) && mlocal_name(t_n) == mlocal_name(s_n))
+        return true;
+
+    // At this point, t_n and s_n are in weak head normal form (modulo meta-variables and proof irrelevance)
+    if (is_def_eq_app(t_n, s_n))
+        return true;
+
+    if (try_eta_expansion(t_n, s_n))
+        return true;
+
+    if (is_def_eq_proof_irrel(t, s))
+        return true;
+
+    return false;
+}
+
+bool type_checker::is_def_eq(expr const & t, expr const & s) {
+    bool r = is_def_eq_core(t, s);
+    if (r)
+        m_eqv_manager.add_equiv(t, s);
+    return r;
 }
 
 type_checker::type_checker(environment const & env, bool memoize):
-    type_checker(env, std::unique_ptr<converter>(new default_converter(env, memoize)), memoize) {}
+    m_env(env), m_memoize(memoize), m_params(nullptr) {
+}
 
 type_checker::~type_checker() {}
 
-optional<expr> type_checker::is_stuck(expr const & e) {
-    return m_conv->is_stuck(e, *this);
-}
-
 void check_no_metavar(environment const & env, name const & n, expr const & e, bool is_type) {
     if (has_metavar(e))
         throw_kernel_exception(env, e, [=](formatter const & fmt) { return pp_decl_has_metavars(fmt, n, e, is_type); });
@@ -338,13 +775,13 @@ static void check_duplicated_params(environment const & env, declaration const &
     }
 }
 
-certified_declaration check(environment const & env, declaration const & d, name_predicate const & pred) {
+certified_declaration check(environment const & env, declaration const & d) {
     if (d.is_definition())
         check_no_mlocal(env, d.get_name(), d.get_value(), false);
     check_no_mlocal(env, d.get_name(), d.get_type(), true);
     check_name(env, d.get_name());
     check_duplicated_params(env, d);
-    type_checker checker(env, std::unique_ptr<converter>(new hint_converter<default_converter>(env, pred)));
+    type_checker checker(env);
     expr sort = checker.check(d.get_type(), d.get_univ_params());
     checker.ensure_sort(sort, d.get_type());
     if (d.is_definition()) {
@@ -358,13 +795,11 @@ certified_declaration check(environment const & env, declaration const & d, name
     return certified_declaration(env.get_id(), d);
 }
 
-certified_declaration check(environment const & env, declaration const & d) {
-    return check(env, d, [](name const &) { return false; });
-}
-
 void initialize_type_checker() {
+    g_dont_care = new expr(Const("dontcare"));
 }
 
 void finalize_type_checker() {
+    delete g_dont_care;
 }
 }
diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h
index d49097e6d8..dad34bf165 100644
--- a/src/kernel/type_checker.h
+++ b/src/kernel/type_checker.h
@@ -5,15 +5,18 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include <unordered_set>
 #include <memory>
 #include <utility>
 #include <algorithm>
+#include "util/lbool.h"
 #include "util/flet.h"
 #include "util/name_set.h"
 #include "util/fresh_name.h"
 #include "kernel/environment.h"
-#include "kernel/converter.h"
+#include "kernel/expr_pair.h"
 #include "kernel/expr_maps.h"
+#include "kernel/equiv_manager.h"
 #include "kernel/abstract_type_context.h"
 
 namespace lean {
@@ -25,13 +28,16 @@ class type_checker : public abstract_type_context {
        The type of (lambda x : A, t)   is (Pi x : A, typeof(t))
        The type of (lambda {x : A}, t) is (Pi {x : A}, typeof(t)) */
     typedef expr_bi_struct_map<expr> cache;
-    environment                m_env;
-    std::unique_ptr<converter> m_conv;
-    cache                      m_infer_type_cache[2];
-    bool                       m_memoize;
-    level_param_names const *  m_params;
+    typedef std::unordered_set<expr_pair, expr_pair_hash, expr_pair_eq> expr_pair_set;
+    environment               m_env;
+    bool                      m_memoize;
+    cache                     m_infer_type_cache[2];
+    expr_struct_map<expr>     m_whnf_core_cache;
+    expr_struct_map<expr>     m_whnf_cache;
+    equiv_manager             m_eqv_manager;
+    expr_pair_set             m_failure_cache;
+    level_param_names const * m_params;
 
-    friend class converter; // allow converter to access the following methods
     pair<expr, expr> open_binding_body(expr const & e);
     expr ensure_sort_core(expr e, expr const & s);
     expr ensure_pi_core(expr e, expr const & s);
@@ -44,12 +50,36 @@ class type_checker : public abstract_type_context {
     expr infer_let(expr const & e, bool infer_only);
     expr infer_type_core(expr const & e, bool infer_only);
     expr infer_type(expr const & e);
-public:
-    /** \brief Create a type checker for the given environment. The auxiliary names created by this
-       type checker are based on the given name generator.
 
+    enum class reduction_status { Continue, DefUnknown, DefEqual, DefDiff };
+    optional<expr> norm_ext(expr const & e);
+    expr whnf_core(expr const & e);
+    expr unfold_name_core(expr e, unsigned h);
+    expr unfold_names(expr const & e, unsigned h);
+    optional<declaration> is_delta(expr const & e) const;
+    expr whnf_core(expr e, unsigned h);
+    bool is_def_eq_binding(expr t, expr s);
+    bool is_def_eq(level const & l1, level const & l2);
+    bool is_def_eq(levels const & ls1, levels const & ls2);
+    lbool quick_is_def_eq(expr const & t, expr const & s, bool use_hash = false);
+    bool is_def_eq_args(expr t, expr s);
+    bool try_eta_expansion_core(expr const & t, expr const & s);
+    bool try_eta_expansion(expr const & t, expr const & s) {
+        return try_eta_expansion_core(t, s) || try_eta_expansion_core(s, t);
+    }
+    bool is_def_eq_app(expr const & t, expr const & s);
+    bool is_def_eq_proof_irrel(expr const & t, expr const & s);
+    bool failed_before(expr const & t, expr const & s) const;
+    void cache_failure(expr const & t, expr const & s);
+    reduction_status lazy_delta_reduction_step(expr & t_n, expr & s_n);
+    lbool lazy_delta_reduction(expr & t_n, expr & s_n);
+    reduction_status ext_reduction_step(expr & t_n, expr & s_n);
+    lbool reduce_def_eq(expr & t_n, expr & s_n);
+    bool is_def_eq_core(expr const & t, expr const & s);
+
+public:
+    /** \brief Create a type checker for the given environment.
        memoize: if true, then inferred types are memoized/cached */
-    type_checker(environment const & env, std::unique_ptr<converter> && conv, bool memoize = true);
     type_checker(environment const & env, bool memoize = true);
     ~type_checker();
 
@@ -96,18 +126,9 @@ public:
 
     optional<expr> expand_macro(expr const & m);
 
-    /** \brief Return true iff \c d is opaque with respect to this type checker. */
-    bool is_opaque(declaration const & d) const;
-    /** \brief Return true iff the constant \c c is opaque with respect to this type checker. */
-    bool is_opaque(expr const & c) const;
-
     /** \brief Return a metavariable that may be stucking the \c e's reduction. */
     virtual optional<expr> is_stuck(expr const & e);
 
-    optional<declaration> is_delta(expr const & e) const { return m_conv->is_delta(e); }
-
-    bool may_reduce_later(expr const & e) { return !is_meta(e) && static_cast<bool>(m_conv->is_stuck(e, *this)); }
-
     template<typename F>
     typename std::result_of<F()>::type with_params(level_param_names const & ps, F && f) {
         flet<level_param_names const *> updt(m_params, &ps);
@@ -122,7 +143,6 @@ void check_no_metavar(environment const & env, name const & n, expr const & e, b
 /** \brief Type check the given declaration, and return a certified declaration if it is type correct.
     Throw an exception if the declaration is type incorrect. */
 certified_declaration check(environment const & env, declaration const & d);
-certified_declaration check(environment const & env, declaration const & d, name_predicate const & opaque_hints);
 
 void initialize_type_checker();
 void finalize_type_checker();
diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp
index 55966f3cf2..c1c8b6b7a3 100644
--- a/src/library/tactic/expr_to_tactic.cpp
+++ b/src/library/tactic/expr_to_tactic.cpp
@@ -9,7 +9,6 @@ Author: Leonardo de Moura
 #include "util/sstream.h"
 #include "util/optional.h"
 #include "kernel/instantiate.h"
-#include "kernel/default_converter.h"
 #include "library/annotation.h"
 #include "library/string.h"
 #include "library/explicit.h"
diff --git a/src/library/tactic/induction_tactic.cpp b/src/library/tactic/induction_tactic.cpp
index 1fa6ffb4b9..7f3dfff975 100644
--- a/src/library/tactic/induction_tactic.cpp
+++ b/src/library/tactic/induction_tactic.cpp
@@ -7,7 +7,6 @@ Author: Leonardo de Moura
 #include "kernel/abstract.h"
 #include "kernel/instantiate.h"
 #include "kernel/inductive/inductive.h"
-#include "kernel/default_converter.h"
 #include "library/util.h"
 #include "library/user_recursors.h"
 #include "library/constants.h"
diff --git a/src/library/util.cpp b/src/library/util.cpp
index 35482b423a..c61298df4c 100644
--- a/src/library/util.cpp
+++ b/src/library/util.cpp
@@ -9,7 +9,6 @@ Author: Leonardo de Moura
 #include "kernel/instantiate.h"
 #include "kernel/error_msgs.h"
 #include "kernel/abstract.h"
-#include "kernel/default_converter.h"
 #include "kernel/inductive/inductive.h"
 #include "library/metavar.h"
 #include "library/locals.h"