diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt
index 766c3f9be..6f46e2e02 100644
--- a/src/kernel/CMakeLists.txt
+++ b/src/kernel/CMakeLists.txt
@@ -3,6 +3,7 @@ replace_fn.cpp free_vars.cpp abstract.cpp instantiate.cpp
 formatter.cpp declaration.cpp environment.cpp
 justification.cpp pos_info_provider.cpp metavar.cpp converter.cpp
 constraint.cpp type_checker.cpp error_msgs.cpp kernel_exception.cpp
-normalizer_extension.cpp init_module.cpp extension_context.cpp expr_cache.cpp)
+normalizer_extension.cpp init_module.cpp extension_context.cpp expr_cache.cpp
+default_converter.cpp)
 
 target_link_libraries(kernel ${LEAN_LIBS})
diff --git a/src/kernel/converter.cpp b/src/kernel/converter.cpp
index 97d2b6018..50b528bcc 100644
--- a/src/kernel/converter.cpp
+++ b/src/kernel/converter.cpp
@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "kernel/instantiate.h"
 #include "kernel/free_vars.h"
 #include "kernel/type_checker.h"
+#include "kernel/default_converter.h"
 
 namespace lean {
 // Temporary hack for ignoring opaque annotations in the kernel
@@ -112,514 +113,6 @@ std::unique_ptr<converter> mk_dummy_converter() {
 name converter::mk_fresh_name(type_checker & tc) { return tc.mk_fresh_name(); }
 pair<expr, constraint_seq> converter::infer_type(type_checker & tc, expr const & e) { return tc.infer_type(e); }
 extension_context & converter::get_extension(type_checker & tc) { return tc.get_extension(); }
-static expr * g_dont_care = nullptr;
-
-struct default_converter : public converter {
-    environment                                 m_env;
-    optional<module_idx>                        m_module_idx;
-    bool                                        m_memoize;
-    extra_opaque_pred                           m_extra_pred;
-    expr_struct_map<expr>                       m_whnf_core_cache;
-    expr_struct_map<pair<expr, constraint_seq>> m_whnf_cache;
-
-    default_converter(environment const & env, optional<module_idx> mod_idx, bool memoize,
-                      extra_opaque_pred const & pred):
-        m_env(env), m_module_idx(mod_idx), m_memoize(memoize), m_extra_pred(pred) {
-    }
-
-    constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j) {
-        return ::lean::mk_eq_cnstr(lhs, rhs, j, static_cast<bool>(m_module_idx));
-    }
-
-    optional<expr> expand_macro(expr const & m, type_checker & c) {
-        lean_assert(is_macro(m));
-        return macro_def(m).expand(m, get_extension(c));
-    }
-
-    /** \brief Apply normalizer extensions to \c e. */
-    optional<pair<expr, constraint_seq>> norm_ext(expr const & e, type_checker & c) {
-        return m_env.norm_ext()(e, get_extension(c));
-    }
-
-    optional<expr> d_norm_ext(expr const & e, type_checker & c, constraint_seq & cs) {
-        if (auto r = norm_ext(e, c)) {
-            cs = cs + r->second;
-            return some_expr(r->first);
-        } else {
-            return none_expr();
-        }
-    }
-
-    /** \brief Return true if \c e may be reduced later after metavariables are instantiated. */
-    bool may_reduce_later(expr const & e, type_checker & c) {
-        return static_cast<bool>(m_env.norm_ext().may_reduce_later(e, get_extension(c)));
-    }
-
-    /** \brief Weak head normal form core procedure. It does not perform delta reduction nor normalization extensions. */
-    expr whnf_core(expr const & e, type_checker & c) {
-        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:
-            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, c))
-                r = whnf_core(*m, c);
-            else
-                r = e;
-            break;
-        case expr_kind::App: {
-            buffer<expr> args;
-            expr f0 = get_app_rev_args(e, args);
-            expr f = whnf_core(f0, c);
-            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()), c);
-            } else {
-                r = f == f0 ? e : whnf_core(mk_rev_app(f, args.size(), args.data()), c);
-            }
-            break;
-        }}
-
-        if (m_memoize)
-            m_whnf_core_cache.insert(mk_pair(e, r));
-        return r;
-    }
-
-    bool is_opaque_core(declaration const & d) const {
-        return ::lean::is_opaque(d, m_extra_pred, m_module_idx);
-    }
-
-    virtual bool is_opaque(declaration const & d) const {
-        return is_opaque_core(d);
-    }
-
-    /** \brief Expand \c e if it is non-opaque constant with weight >= w */
-    expr unfold_name_core(expr e, unsigned w) {
-        if (is_constant(e)) {
-            if (auto d = m_env.find(const_name(e))) {
-                if (d->is_definition() && !is_opaque_core(*d) && d->get_weight() >= w)
-                    return unfold_name_core(instantiate_value_univ_params(*d, const_levels(e)), w);
-            }
-        }
-        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 weight >= w.
-    */
-    expr unfold_names(expr const & e, unsigned w) {
-        if (is_app(e)) {
-            expr f0 = get_app_fn(e);
-            expr f  = unfold_name_core(f0, w);
-            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, w);
-        }
-    }
-
-    /**
-        \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> is_delta(expr const & e) {
-        return ::lean::is_delta(m_env, get_app_fn(e), m_extra_pred, m_module_idx);
-    }
-
-    /**
-        \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, type_checker & c) {
-        while (true) {
-            expr new_e = unfold_names(whnf_core(e, c), w);
-            if (is_eqp(e, new_e))
-                return e;
-            e = new_e;
-        }
-    }
-
-    /** \brief Put expression \c t in weak head normal form */
-    virtual pair<expr, constraint_seq> whnf(expr const & e_prime, type_checker & c) {
-        // 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 to_ecs(e_prime);
-        case expr_kind::Lambda: case expr_kind::Macro: case expr_kind::App: case expr_kind::Constant:
-            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;
-        constraint_seq cs;
-        while (true) {
-            expr t1 = whnf_core(t, 0, c);
-            if (auto new_t = d_norm_ext(t1, c, cs)) {
-                t  = *new_t;
-            } else {
-                auto r = mk_pair(t1, cs);
-                if (m_memoize)
-                    m_whnf_cache.insert(mk_pair(e, r));
-                return r;
-            }
-        }
-    }
-
-    expr whnf(expr const & e_prime, type_checker & c, constraint_seq & cs) {
-        auto r = whnf(e_prime, c);
-        cs = cs + r.second;
-        return r.first;
-    }
-
-    pair<bool, constraint_seq> to_bcs(bool b) { return mk_pair(b, constraint_seq()); }
-    pair<bool, constraint_seq> to_bcs(bool b, constraint const & c) { return mk_pair(b, constraint_seq(c)); }
-    pair<bool, constraint_seq> to_bcs(bool b, constraint_seq const & cs) { return mk_pair(b, cs); }
-
-    /**
-        \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 is_def_eq_binding(expr t, expr s, type_checker & c, delayed_justification & jst, constraint_seq & cs) {
-        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, c, jst, cs))
-                    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(c), 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()), c, jst, cs);
-    }
-
-    bool is_def_eq(level const & l1, level const & l2, delayed_justification & jst, constraint_seq & cs) {
-        if (is_equivalent(l1, l2)) {
-            return true;
-        } else if (has_meta(l1) || has_meta(l2)) {
-            cs = cs + constraint_seq(mk_level_eq_cnstr(l1, l2, jst.get()));
-            return true;
-        } else {
-            return false;
-        }
-    }
-
-    bool is_def_eq(levels const & ls1, levels const & ls2, type_checker & c, delayed_justification & jst, constraint_seq & cs) {
-        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), jst, cs) &&
-                is_def_eq(tail(ls1), tail(ls2), c, jst, cs);
-        } else {
-            return false;
-        }
-    }
-
-    static pair<lbool, constraint_seq> to_lbcs(lbool l) { return mk_pair(l, constraint_seq()); }
-    static pair<lbool, constraint_seq> to_lbcs(lbool l, constraint const & c) { return mk_pair(l, constraint_seq(c)); }
-    static pair<lbool, constraint_seq> to_lbcs(pair<bool, constraint_seq> const & bcs) {
-        return mk_pair(to_lbool(bcs.first), bcs.second);
-    }
-
-    /** \brief This is an auxiliary method for is_def_eq. It handles the "easy cases". */
-    lbool quick_is_def_eq(expr const & t, expr const & s, type_checker & c, delayed_justification & jst, constraint_seq & cs) {
-        if (t == s)
-            return l_true; // t and s are structurally equal
-        if (is_meta(t) || is_meta(s)) {
-            // if t or s is a metavariable (or the application of a metavariable), then add constraint
-            cs = cs + constraint_seq(mk_eq_cnstr(t, s, jst.get()));
-            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, c, jst, cs));
-            case expr_kind::Sort:
-                return to_lbool(is_def_eq(sort_level(t), sort_level(s), c, jst, cs));
-            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:
-                // 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 is_def_eq_args(expr t, expr s, type_checker & c, delayed_justification & jst, constraint_seq & cs) {
-        while (is_app(t) && is_app(s)) {
-            if (!is_def_eq(app_arg(t), app_arg(s), c, jst, cs))
-                return false;
-            t = app_fn(t);
-            s = app_fn(s);
-        }
-        return !is_app(t) && !is_app(s);
-    }
-
-    /** \brief Return true iff t is a constant named f_name or an application of the form (f_name a_1 ... a_k) */
-    bool is_app_of(expr t, name const & f_name) {
-        t = get_app_fn(t);
-        return is_constant(t) && const_name(t) == f_name;
-    }
-
-    /** \brief Try to solve (fun (x : A), B) =?= s by trying eta-expansion on s */
-    bool try_eta_expansion(expr const & t, expr const & s, type_checker & c, delayed_justification & jst, constraint_seq & cs) {
-        if (is_lambda(t) && !is_lambda(s)) {
-            auto tcs    = infer_type(c, s);
-            auto wcs    = whnf(tcs.first, c);
-            expr s_type = wcs.first;
-            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));
-            auto dcs    = is_def_eq(t, new_s, c, jst);
-            if (!dcs.first)
-                return false;
-            cs = cs + dcs.second + wcs.second + tcs.second;
-            return true;
-        } else {
-            return false;
-        }
-    }
-
-    bool is_def_eq(expr const & t, expr const & s, type_checker & c, delayed_justification & jst, constraint_seq & cs) {
-        auto bcs = is_def_eq(t, s, c, jst);
-        if (bcs.first) {
-            cs = cs + bcs.second;
-            return true;
-        } else {
-            return false;
-        }
-    }
-
-    /** Return true iff t is definitionally equal to s. */
-    virtual pair<bool, constraint_seq> is_def_eq(expr const & t, expr const & s, type_checker & c, delayed_justification & jst) {
-        check_system("is_definitionally_equal");
-        constraint_seq cs;
-        lbool r = quick_is_def_eq(t, s, c, jst, cs);
-        if (r != l_undef) return to_bcs(r == l_true, cs);
-
-        // apply whnf (without using delta-reduction or normalizer extensions)
-        expr t_n = whnf_core(t, c);
-        expr s_n = whnf_core(s, c);
-
-        if (!is_eqp(t_n, t) || !is_eqp(s_n, s)) {
-            r = quick_is_def_eq(t_n, s_n, c, jst, cs);
-            if (r != l_undef) return to_bcs(r == l_true, cs);
-        }
-
-        // lazy delta-reduction and then normalizer extensions
-        while (true) {
-            // first, keep applying lazy delta-reduction while applicable
-            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), c);
-                } else if (!d_t && d_s) {
-                    s_n = whnf_core(unfold_names(s_n, 0), c);
-                } else if (d_t->get_weight() > d_s->get_weight()) {
-                    t_n = whnf_core(unfold_names(t_n, d_s->get_weight() + 1), c);
-                } else if (d_t->get_weight() < d_s->get_weight()) {
-                    s_n = whnf_core(unfold_names(s_n, d_t->get_weight() + 1), c);
-                } 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)) {
-                        // 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
-                            break;
-                        } 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_core(*d_t) && d_t->use_conv_opt() &&
-                                is_def_eq_args(t_n, s_n, c, jst, cs))
-                                return to_bcs(true, cs);
-                        }
-                    }
-                    t_n = whnf_core(unfold_names(t_n, d_t->get_weight() - 1), c);
-                    s_n = whnf_core(unfold_names(s_n, d_s->get_weight() - 1), c);
-                }
-                r = quick_is_def_eq(t_n, s_n, c, jst, cs);
-                if (r != l_undef) return to_bcs(r == l_true, cs);
-            }
-            // try normalizer extensions
-            auto new_t_n = d_norm_ext(t_n, c, cs);
-            auto new_s_n = d_norm_ext(s_n, c, cs);
-            if (!new_t_n && !new_s_n)
-                break; // t_n and s_n are in weak head normal form
-            if (new_t_n)
-                t_n = whnf_core(*new_t_n, c);
-            if (new_s_n)
-                s_n = whnf_core(*new_s_n, c);
-            r = quick_is_def_eq(t_n, s_n, c, jst, cs);
-            if (r != l_undef) return to_bcs(r == l_true, cs);
-        }
-
-        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), c, jst, cs))
-            return to_bcs(true, cs);
-
-        if (is_local(t_n) && is_local(s_n) && mlocal_name(t_n) == mlocal_name(s_n))
-            return to_bcs(true, cs);
-
-        optional<declaration> d_t, d_s;
-        bool delay_check = false;
-        if (has_expr_metavar(t_n) || has_expr_metavar(s_n)) {
-            d_t = is_delta(t_n);
-            d_s = is_delta(s_n);
-            if (d_t && d_s && is_eqp(*d_t, *d_s))
-                delay_check = true;
-            else if (may_reduce_later(t_n, c) && may_reduce_later(s_n, c))
-                delay_check = true;
-        }
-
-        // At this point, t_n and s_n are in weak head normal form (modulo meta-variables and proof irrelevance)
-        if (!delay_check && is_app(t_n) && is_app(s_n)) {
-            buffer<expr> t_args;
-            buffer<expr> s_args;
-            expr t_fn = get_app_args(t_n, t_args);
-            expr s_fn = get_app_args(s_n, s_args);
-            constraint_seq cs_prime = cs;
-            if (is_def_eq(t_fn, s_fn, c, jst, cs_prime) && 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], c, jst, cs_prime))
-                        break;
-                }
-                if (i == t_args.size()) {
-                    return to_bcs(true, cs_prime);
-                }
-            }
-        }
-
-        if (try_eta_expansion(t_n, s_n, c, jst, cs) ||
-            try_eta_expansion(s_n, t_n, c, jst, cs))
-            return to_bcs(true, cs);
-
-        if (m_env.prop_proof_irrel()) {
-            // Proof irrelevance support for Prop (aka Type.{0})
-            auto tcs    = infer_type(c, t);
-            auto scs    = infer_type(c, s);
-            expr t_type = tcs.first;
-            expr s_type = scs.first;
-            // remark: is_prop returns true only if t_type reducible to Prop.
-            // If t_type contains metavariables, then reduction can get stuck, and is_prop will return false.
-            auto pcs    = is_prop(t_type, c);
-            if (pcs.first) {
-                auto dcs = is_def_eq(t_type, s_type, c, jst);
-                if (dcs.first)
-                    return to_bcs(true, dcs.second + scs.second + pcs.second + tcs.second);
-            } else {
-                // If we can't stablish whether t_type is Prop, we try s_type.
-                pcs = is_prop(s_type, c);
-                if (pcs.first) {
-                    auto dcs = is_def_eq(t_type, s_type, c, jst);
-                    if (dcs.first)
-                        return to_bcs(true, dcs.second + scs.second + pcs.second + tcs.second);
-                }
-                // This procedure will miss the case where s_type and t_type cannot be reduced to Prop
-                // because they contain metavariables.
-            }
-        }
-
-        if (may_reduce_later(t_n, c) || may_reduce_later(s_n, c) || delay_check) {
-            cs = cs + constraint_seq(mk_eq_cnstr(t_n, s_n, jst.get()));
-            return to_bcs(true, cs);
-        }
-
-        return to_bcs(false);
-    }
-
-    pair<bool, constraint_seq> is_prop(expr const & e, type_checker & c) {
-        auto tcs = infer_type(c, e);
-        auto wcs = whnf(tcs.first, c);
-        if (wcs.first == mk_Prop())
-            return to_bcs(true, wcs.second + tcs.second);
-        else
-            return to_bcs(false);
-    }
-
-    virtual optional<module_idx> get_module_idx() const {
-        return m_module_idx;
-    }
-};
 
 std::unique_ptr<converter> mk_default_converter(environment const & env, optional<module_idx> mod_idx,
                                                 bool memoize, extra_opaque_pred const & pred) {
@@ -643,12 +136,10 @@ std::unique_ptr<converter> mk_default_converter(environment const & env, bool un
 void initialize_converter() {
     g_opt_main_module_idx = new optional<module_idx>(g_main_module_idx);
     g_no_delayed_jst      = new no_delayed_justification();
-    g_dont_care           = new expr(Const("dontcare"));
 }
 
 void finalize_converter() {
     delete g_opt_main_module_idx;
     delete g_no_delayed_jst;
-    delete g_dont_care;
 }
 }
diff --git a/src/kernel/default_converter.cpp b/src/kernel/default_converter.cpp
new file mode 100644
index 000000000..fbf368ace
--- /dev/null
+++ b/src/kernel/default_converter.cpp
@@ -0,0 +1,508 @@
+/*
+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 "kernel/default_converter.h"
+#include "kernel/instantiate.h"
+#include "kernel/free_vars.h"
+#include "kernel/type_checker.h"
+
+namespace lean {
+static expr * g_dont_care = nullptr;
+
+default_converter::default_converter(environment const & env, optional<module_idx> mod_idx, bool memoize,
+                                     extra_opaque_pred const & pred):
+    m_env(env), m_module_idx(mod_idx), m_memoize(memoize), m_extra_pred(pred) {
+}
+
+constraint default_converter::mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j) {
+    return ::lean::mk_eq_cnstr(lhs, rhs, j, static_cast<bool>(m_module_idx));
+}
+
+optional<expr> default_converter::expand_macro(expr const & m, type_checker & c) {
+    lean_assert(is_macro(m));
+    return macro_def(m).expand(m, get_extension(c));
+}
+
+/** \brief Apply normalizer extensions to \c e. */
+optional<pair<expr, constraint_seq>> default_converter::norm_ext(expr const & e, type_checker & c) {
+    return m_env.norm_ext()(e, get_extension(c));
+}
+
+optional<expr> default_converter::d_norm_ext(expr const & e, type_checker & c, constraint_seq & cs) {
+    if (auto r = norm_ext(e, c)) {
+        cs = cs + r->second;
+        return some_expr(r->first);
+    } else {
+        return none_expr();
+    }
+}
+
+/** \brief Return true if \c e may be reduced later after metavariables are instantiated. */
+bool default_converter::may_reduce_later(expr const & e, type_checker & c) {
+    return static_cast<bool>(m_env.norm_ext().may_reduce_later(e, get_extension(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, type_checker & c) {
+    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:
+        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, c))
+            r = whnf_core(*m, c);
+        else
+            r = e;
+        break;
+    case expr_kind::App: {
+        buffer<expr> args;
+        expr f0 = get_app_rev_args(e, args);
+        expr f = whnf_core(f0, c);
+        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()), c);
+        } else {
+            r = f == f0 ? e : whnf_core(mk_rev_app(f, args.size(), args.data()), c);
+        }
+        break;
+    }}
+
+    if (m_memoize)
+        m_whnf_core_cache.insert(mk_pair(e, r));
+    return r;
+}
+
+bool default_converter::is_opaque_core(declaration const & d) const {
+    return ::lean::is_opaque(d, m_extra_pred, m_module_idx);
+}
+
+bool default_converter::is_opaque(declaration const & d) const {
+    return is_opaque_core(d);
+}
+
+/** \brief Expand \c e if it is non-opaque constant with weight >= w */
+expr default_converter::unfold_name_core(expr e, unsigned w) {
+    if (is_constant(e)) {
+        if (auto d = m_env.find(const_name(e))) {
+            if (d->is_definition() && !is_opaque_core(*d) && d->get_weight() >= w)
+                return unfold_name_core(instantiate_value_univ_params(*d, const_levels(e)), w);
+        }
+    }
+    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 weight >= w.
+*/
+expr default_converter::unfold_names(expr const & e, unsigned w) {
+    if (is_app(e)) {
+        expr f0 = get_app_fn(e);
+        expr f  = unfold_name_core(f0, w);
+        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, w);
+    }
+}
+
+/**
+   \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) {
+    return ::lean::is_delta(m_env, get_app_fn(e), m_extra_pred, m_module_idx);
+}
+
+/**
+   \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 default_converter::whnf_core(expr e, unsigned w, type_checker & c) {
+    while (true) {
+        expr new_e = unfold_names(whnf_core(e, c), w);
+        if (is_eqp(e, new_e))
+            return e;
+        e = new_e;
+    }
+}
+
+/** \brief Put expression \c t in weak head normal form */
+pair<expr, constraint_seq> default_converter::whnf(expr const & e_prime, type_checker & c) {
+    // 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 to_ecs(e_prime);
+    case expr_kind::Lambda: case expr_kind::Macro: case expr_kind::App: case expr_kind::Constant:
+        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;
+    constraint_seq cs;
+    while (true) {
+        expr t1 = whnf_core(t, 0, c);
+        if (auto new_t = d_norm_ext(t1, c, cs)) {
+            t  = *new_t;
+        } else {
+            auto r = mk_pair(t1, cs);
+            if (m_memoize)
+                m_whnf_cache.insert(mk_pair(e, r));
+            return r;
+        }
+    }
+}
+
+expr default_converter::whnf(expr const & e_prime, type_checker & c, constraint_seq & cs) {
+    auto r = whnf(e_prime, c);
+    cs = cs + r.second;
+    return r.first;
+}
+
+
+/**
+   \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, type_checker & c, delayed_justification & jst, constraint_seq & cs) {
+    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, c, jst, cs))
+                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(c), 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()), c, jst, cs);
+}
+
+bool default_converter::is_def_eq(level const & l1, level const & l2, delayed_justification & jst, constraint_seq & cs) {
+    if (is_equivalent(l1, l2)) {
+        return true;
+    } else if (has_meta(l1) || has_meta(l2)) {
+        cs = cs + constraint_seq(mk_level_eq_cnstr(l1, l2, jst.get()));
+        return true;
+    } else {
+        return false;
+    }
+}
+
+bool default_converter::is_def_eq(levels const & ls1, levels const & ls2, type_checker & c, delayed_justification & jst, constraint_seq & cs) {
+    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), jst, cs) &&
+            is_def_eq(tail(ls1), tail(ls2), c, jst, cs);
+    } 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, type_checker & c, delayed_justification & jst, constraint_seq & cs) {
+    if (t == s)
+        return l_true; // t and s are structurally equal
+    if (is_meta(t) || is_meta(s)) {
+        // if t or s is a metavariable (or the application of a metavariable), then add constraint
+        cs = cs + constraint_seq(mk_eq_cnstr(t, s, jst.get()));
+        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, c, jst, cs));
+        case expr_kind::Sort:
+            return to_lbool(is_def_eq(sort_level(t), sort_level(s), c, jst, cs));
+        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:
+            // 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, type_checker & c, delayed_justification & jst, constraint_seq & cs) {
+    while (is_app(t) && is_app(s)) {
+        if (!is_def_eq(app_arg(t), app_arg(s), c, jst, cs))
+            return false;
+        t = app_fn(t);
+        s = app_fn(s);
+    }
+    return !is_app(t) && !is_app(s);
+}
+
+/** \brief Return true iff t is a constant named f_name or an application of the form (f_name a_1 ... a_k) */
+bool default_converter::is_app_of(expr t, name const & f_name) {
+    t = get_app_fn(t);
+    return is_constant(t) && const_name(t) == f_name;
+}
+
+/** \brief Try to solve (fun (x : A), B) =?= s by trying eta-expansion on s */
+bool default_converter::try_eta_expansion(expr const & t, expr const & s, type_checker & c, delayed_justification & jst, constraint_seq & cs) {
+    if (is_lambda(t) && !is_lambda(s)) {
+        auto tcs    = infer_type(c, s);
+        auto wcs    = whnf(tcs.first, c);
+        expr s_type = wcs.first;
+        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));
+        auto dcs    = is_def_eq(t, new_s, c, jst);
+        if (!dcs.first)
+            return false;
+        cs = cs + dcs.second + wcs.second + tcs.second;
+        return true;
+    } else {
+        return false;
+    }
+}
+
+bool default_converter::is_def_eq(expr const & t, expr const & s, type_checker & c, delayed_justification & jst, constraint_seq & cs) {
+    auto bcs = is_def_eq(t, s, c, jst);
+    if (bcs.first) {
+        cs = cs + bcs.second;
+        return true;
+    } else {
+        return false;
+    }
+}
+
+/** Return true iff t is definitionally equal to s. */
+pair<bool, constraint_seq> default_converter::is_def_eq(expr const & t, expr const & s, type_checker & c, delayed_justification & jst) {
+    check_system("is_definitionally_equal");
+    constraint_seq cs;
+    lbool r = quick_is_def_eq(t, s, c, jst, cs);
+    if (r != l_undef) return to_bcs(r == l_true, cs);
+
+    // apply whnf (without using delta-reduction or normalizer extensions)
+    expr t_n = whnf_core(t, c);
+    expr s_n = whnf_core(s, c);
+
+    if (!is_eqp(t_n, t) || !is_eqp(s_n, s)) {
+        r = quick_is_def_eq(t_n, s_n, c, jst, cs);
+        if (r != l_undef) return to_bcs(r == l_true, cs);
+    }
+
+    // lazy delta-reduction and then normalizer extensions
+    while (true) {
+        // first, keep applying lazy delta-reduction while applicable
+        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), c);
+            } else if (!d_t && d_s) {
+                s_n = whnf_core(unfold_names(s_n, 0), c);
+            } else if (d_t->get_weight() > d_s->get_weight()) {
+                t_n = whnf_core(unfold_names(t_n, d_s->get_weight() + 1), c);
+            } else if (d_t->get_weight() < d_s->get_weight()) {
+                s_n = whnf_core(unfold_names(s_n, d_t->get_weight() + 1), c);
+            } 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)) {
+                    // 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
+                        break;
+                    } 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_core(*d_t) && d_t->use_conv_opt() &&
+                            is_def_eq_args(t_n, s_n, c, jst, cs))
+                            return to_bcs(true, cs);
+                    }
+                }
+                t_n = whnf_core(unfold_names(t_n, d_t->get_weight() - 1), c);
+                s_n = whnf_core(unfold_names(s_n, d_s->get_weight() - 1), c);
+            }
+            r = quick_is_def_eq(t_n, s_n, c, jst, cs);
+            if (r != l_undef) return to_bcs(r == l_true, cs);
+        }
+        // try normalizer extensions
+        auto new_t_n = d_norm_ext(t_n, c, cs);
+        auto new_s_n = d_norm_ext(s_n, c, cs);
+        if (!new_t_n && !new_s_n)
+            break; // t_n and s_n are in weak head normal form
+        if (new_t_n)
+            t_n = whnf_core(*new_t_n, c);
+        if (new_s_n)
+            s_n = whnf_core(*new_s_n, c);
+        r = quick_is_def_eq(t_n, s_n, c, jst, cs);
+        if (r != l_undef) return to_bcs(r == l_true, cs);
+    }
+
+    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), c, jst, cs))
+        return to_bcs(true, cs);
+
+    if (is_local(t_n) && is_local(s_n) && mlocal_name(t_n) == mlocal_name(s_n))
+        return to_bcs(true, cs);
+
+    optional<declaration> d_t, d_s;
+    bool delay_check = false;
+    if (has_expr_metavar(t_n) || has_expr_metavar(s_n)) {
+        d_t = is_delta(t_n);
+        d_s = is_delta(s_n);
+        if (d_t && d_s && is_eqp(*d_t, *d_s))
+            delay_check = true;
+        else if (may_reduce_later(t_n, c) && may_reduce_later(s_n, c))
+            delay_check = true;
+    }
+
+    // At this point, t_n and s_n are in weak head normal form (modulo meta-variables and proof irrelevance)
+    if (!delay_check && is_app(t_n) && is_app(s_n)) {
+        buffer<expr> t_args;
+        buffer<expr> s_args;
+        expr t_fn = get_app_args(t_n, t_args);
+        expr s_fn = get_app_args(s_n, s_args);
+        constraint_seq cs_prime = cs;
+        if (is_def_eq(t_fn, s_fn, c, jst, cs_prime) && 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], c, jst, cs_prime))
+                    break;
+            }
+            if (i == t_args.size()) {
+                return to_bcs(true, cs_prime);
+            }
+        }
+    }
+
+    if (try_eta_expansion(t_n, s_n, c, jst, cs) ||
+        try_eta_expansion(s_n, t_n, c, jst, cs))
+        return to_bcs(true, cs);
+
+    if (m_env.prop_proof_irrel()) {
+        // Proof irrelevance support for Prop (aka Type.{0})
+        auto tcs    = infer_type(c, t);
+        auto scs    = infer_type(c, s);
+        expr t_type = tcs.first;
+        expr s_type = scs.first;
+        // remark: is_prop returns true only if t_type reducible to Prop.
+        // If t_type contains metavariables, then reduction can get stuck, and is_prop will return false.
+        auto pcs    = is_prop(t_type, c);
+        if (pcs.first) {
+            auto dcs = is_def_eq(t_type, s_type, c, jst);
+            if (dcs.first)
+                return to_bcs(true, dcs.second + scs.second + pcs.second + tcs.second);
+        } else {
+            // If we can't stablish whether t_type is Prop, we try s_type.
+            pcs = is_prop(s_type, c);
+            if (pcs.first) {
+                auto dcs = is_def_eq(t_type, s_type, c, jst);
+                if (dcs.first)
+                    return to_bcs(true, dcs.second + scs.second + pcs.second + tcs.second);
+            }
+            // This procedure will miss the case where s_type and t_type cannot be reduced to Prop
+            // because they contain metavariables.
+        }
+    }
+
+    if (may_reduce_later(t_n, c) || may_reduce_later(s_n, c) || delay_check) {
+        cs = cs + constraint_seq(mk_eq_cnstr(t_n, s_n, jst.get()));
+        return to_bcs(true, cs);
+    }
+
+    return to_bcs(false);
+}
+
+pair<bool, constraint_seq> default_converter::is_prop(expr const & e, type_checker & c) {
+    auto tcs = infer_type(c, e);
+    auto wcs = whnf(tcs.first, c);
+    if (wcs.first == mk_Prop())
+        return to_bcs(true, wcs.second + tcs.second);
+    else
+        return to_bcs(false);
+}
+
+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
new file mode 100644
index 000000000..f9817597d
--- /dev/null
+++ b/src/kernel/default_converter.h
@@ -0,0 +1,74 @@
+/*
+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 "util/lbool.h"
+#include "kernel/justification.h"
+#include "kernel/environment.h"
+#include "kernel/converter.h"
+#include "kernel/expr_maps.h"
+
+namespace lean {
+/** \breif Converter used in the kernel */
+class default_converter : public converter {
+protected:
+    environment                                 m_env;
+    optional<module_idx>                        m_module_idx;
+    bool                                        m_memoize;
+    extra_opaque_pred                           m_extra_pred;
+    expr_struct_map<expr>                       m_whnf_core_cache;
+    expr_struct_map<pair<expr, constraint_seq>> m_whnf_cache;
+
+    virtual bool may_reduce_later(expr const & e, type_checker & c);
+
+    constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j);
+    optional<expr> expand_macro(expr const & m, type_checker & c);
+    optional<pair<expr, constraint_seq>> norm_ext(expr const & e, type_checker & c);
+    optional<expr> d_norm_ext(expr const & e, type_checker & c, constraint_seq & cs);
+    expr whnf_core(expr const & e, type_checker & c);
+    bool is_opaque_core(declaration const & d) const;
+    expr unfold_name_core(expr e, unsigned w);
+    expr unfold_names(expr const & e, unsigned w);
+    optional<declaration> is_delta(expr const & e);
+    expr whnf_core(expr e, unsigned w, type_checker & c);
+
+    expr whnf(expr const & e_prime, type_checker & c, constraint_seq & cs);
+
+    pair<bool, constraint_seq> to_bcs(bool b) { return mk_pair(b, constraint_seq()); }
+    pair<bool, constraint_seq> to_bcs(bool b, constraint const & c) { return mk_pair(b, constraint_seq(c)); }
+    pair<bool, constraint_seq> to_bcs(bool b, constraint_seq const & cs) { return mk_pair(b, cs); }
+
+    bool is_def_eq_binding(expr t, expr s, type_checker & c, delayed_justification & jst, constraint_seq & cs);
+    bool is_def_eq(level const & l1, level const & l2, delayed_justification & jst, constraint_seq & cs);
+    bool is_def_eq(levels const & ls1, levels const & ls2, type_checker & c, delayed_justification & jst, constraint_seq & cs);
+
+    static pair<lbool, constraint_seq> to_lbcs(lbool l) { return mk_pair(l, constraint_seq()); }
+    static pair<lbool, constraint_seq> to_lbcs(lbool l, constraint const & c) { return mk_pair(l, constraint_seq(c)); }
+    static pair<lbool, constraint_seq> to_lbcs(pair<bool, constraint_seq> const & bcs) {
+        return mk_pair(to_lbool(bcs.first), bcs.second);
+    }
+
+    lbool quick_is_def_eq(expr const & t, expr const & s, type_checker & c, delayed_justification & jst, constraint_seq & cs);
+    bool is_def_eq_args(expr t, expr s, type_checker & c, delayed_justification & jst, constraint_seq & cs);
+    bool is_app_of(expr t, name const & f_name);
+    bool try_eta_expansion(expr const & t, expr const & s, type_checker & c, delayed_justification & jst, constraint_seq & cs);
+    bool is_def_eq(expr const & t, expr const & s, type_checker & c, delayed_justification & jst, constraint_seq & cs);
+
+    pair<bool, constraint_seq> is_prop(expr const & e, type_checker & c);
+
+public:
+    default_converter(environment const & env, optional<module_idx> mod_idx, bool memoize,
+                      extra_opaque_pred const & pred);
+
+    virtual bool is_opaque(declaration const & d) const;
+    virtual pair<expr, constraint_seq> whnf(expr const & e_prime, type_checker & c);
+    virtual optional<module_idx> get_module_idx() const { return m_module_idx; }
+    virtual pair<bool, constraint_seq> is_def_eq(expr const & t, expr const & s, type_checker & c, delayed_justification & jst);
+};
+
+void initialize_default_converter();
+void finalize_default_converter();
+}
diff --git a/src/kernel/init_module.cpp b/src/kernel/init_module.cpp
index 728ecfd1d..cbfd9db52 100644
--- a/src/kernel/init_module.cpp
+++ b/src/kernel/init_module.cpp
@@ -11,12 +11,14 @@ Author: Leonardo de Moura
 #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();
@@ -27,6 +29,7 @@ void finalize_kernel_module() {
     finalize_environment();
     finalize_type_checker();
     finalize_converter();
+    finalize_default_converter();
     finalize_declaration();
     finalize_expr();
     finalize_level();