diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index 7846fb6a4b..96d28f0605 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -7,6 +7,6 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
   standard_kernel.cpp hott_kernel.cpp
   unifier.cpp unifier_plugin.cpp inductive_unifier_plugin.cpp
   explicit.cpp num.cpp string.cpp opaque_hints.cpp head_map.cpp
-  match.cpp)
+  match.cpp definitions_cache.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})
diff --git a/src/library/definitions_cache.cpp b/src/library/definitions_cache.cpp
new file mode 100644
index 0000000000..b22b0f5cd5
--- /dev/null
+++ b/src/library/definitions_cache.cpp
@@ -0,0 +1,163 @@
+/*
+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 "library/placeholder.h"
+#include "library/kernel_serializer.h"
+#include "library/definitions_cache.h"
+
+namespace lean {
+/** \brief Similar to expr_eq_fn, but allows different placeholders
+    with different names. We cannot use the hashcode to speedup comparasion.
+*/
+class expr_eq_modulo_placeholders_fn {
+    name_map<name> m_map; // for comparing placeholder names
+
+    bool compare(name const & a, name const & b, bool placeholders) {
+        if (!placeholders) {
+            return a == b;
+        } else if (auto it = m_map.find(a)) {
+            return *it == b;
+        } else {
+            m_map.insert(a, b);
+            return true;
+        }
+    }
+
+    bool compare(level const & l1, level const & l2) {
+        if (kind(l1) != kind(l2)) return false;
+        if (is_eqp(l1, l2))       return true;
+        bool placeholders = is_placeholder(l1) && is_placeholder(l2);
+        switch (kind(l1)) {
+        case level_kind::Zero:
+            return true;
+        case level_kind::Param:
+            return compare(param_id(l1), param_id(l2), placeholders);
+        case level_kind::Global:
+            return compare(global_id(l1), global_id(l2), placeholders);
+        case level_kind::Meta:
+            return compare(meta_id(l1), meta_id(l2), placeholders);
+        case level_kind::Max:
+            if (get_depth(l1) != get_depth(l2))
+                return false;
+            return
+                compare(max_lhs(l1), max_lhs(l2)) &&
+                compare(max_rhs(l1), max_rhs(l2));
+        case level_kind::IMax:
+            if (get_depth(l1) != get_depth(l2))
+                return false;
+            return
+                compare(imax_lhs(l1), imax_lhs(l2)) &&
+                compare(imax_rhs(l1), imax_rhs(l2));
+        case level_kind::Succ:
+            if (get_depth(l1) != get_depth(l2))
+                return false;
+            return
+                is_explicit(l1) == is_explicit(l2) &&
+                (is_explicit(l1) || compare(succ_of(l1), succ_of(l2)));
+        }
+        lean_unreachable(); // LCOV_EXCL_LINE
+    }
+
+    bool compare(levels const & ls1, levels const & ls2) {
+        return ::lean::compare(ls1, ls2,
+                               [&](level const & l1, level const & l2) { return compare(l1, l2); });
+    }
+
+    bool compare(expr const & a, expr const & b) {
+        if (is_eqp(a, b))                   return true;
+        if (a.kind() != b.kind())           return false;
+        if (get_weight(a) != get_weight(b)) return false;
+        check_system("expression equality modulo placeholder test");
+        bool placeholders = is_placeholder(a) && is_placeholder(b);
+        switch (a.kind()) {
+        case expr_kind::Var:
+            return var_idx(a) == var_idx(b);
+        case expr_kind::Constant:
+            return
+                compare(const_name(a), const_name(b), placeholders) &&
+                compare(const_levels(a), const_levels(b));
+        case expr_kind::Meta:
+            return
+                compare(mlocal_name(a), mlocal_name(b), placeholders) &&
+                compare(mlocal_type(a), mlocal_type(b));
+        case expr_kind::Local:
+            return
+                compare(mlocal_name(a), mlocal_name(b), placeholders) &&
+                compare(mlocal_type(a), mlocal_type(b)) &&
+                local_pp_name(a) == local_pp_name(b) &&
+                local_info(a) == local_info(b);
+        case expr_kind::App:
+            return
+                compare(app_fn(a), app_fn(b)) &&
+                compare(app_arg(a), app_arg(b));
+        case expr_kind::Lambda: case expr_kind::Pi:
+            return
+                compare(binding_domain(a), binding_domain(b)) &&
+                compare(binding_body(a), binding_body(b)) &&
+                binding_info(a) == binding_info(b);
+        case expr_kind::Sort:
+            return compare(sort_level(a), sort_level(b));
+        case expr_kind::Macro:
+            if (macro_def(a) != macro_def(b) || macro_num_args(a) != macro_num_args(b))
+                return false;
+            for (unsigned i = 0; i < macro_num_args(a); i++) {
+                if (!compare(macro_arg(a, i), macro_arg(b, i)))
+                    return false;
+            }
+            return true;
+        }
+        lean_unreachable(); // LCOV_EXCL_LINE
+    }
+
+public:
+    expr_eq_modulo_placeholders_fn() {}
+    bool operator()(expr const & a, expr const & b) { return compare(a, b); }
+};
+
+definitions_cache::definitions_cache() {}
+
+definitions_cache::definitions_cache(std::istream & in) {
+    deserializer d(in);
+    unsigned num;
+    d >> num;
+    for (unsigned i = 0; i < num; i++) {
+        name n;
+        level_param_names ls;
+        expr pre_type, pre_value, type, value;
+        d >> n >> pre_type >> pre_value >> ls >> type >> value;
+        add(n, pre_type, pre_value, ls, type, value);
+    }
+}
+
+void definitions_cache::add(name const & n, expr const & pre_type, expr const & pre_value,
+                            level_param_names const & ls, expr const & type, expr const & value) {
+    m_definitions.insert(n, entry(pre_type, pre_value, ls, type, value));
+}
+
+optional<std::tuple<level_param_names, expr, expr>> definitions_cache::find(name const & n, expr const & pre_type, expr const & pre_value) {
+    if (auto it = m_definitions.find(n)) {
+        level_param_names ls;
+        expr c_pre_type, c_pre_value, type, value;
+        std::tie(c_pre_type, c_pre_value, ls, type, value) = *it;
+        if (expr_eq_modulo_placeholders_fn()(c_pre_type, pre_type) &&
+            expr_eq_modulo_placeholders_fn()(c_pre_value, pre_value))
+            return some(std::make_tuple(ls, type, value));
+    }
+    return optional<std::tuple<level_param_names, expr, expr>>();
+}
+
+void definitions_cache::save(std::ostream & out) {
+    serializer s(out);
+    s << m_definitions.size();
+    m_definitions.for_each([&](name const & n, entry const & e) {
+            level_param_names ls;
+            expr c_pre_type, c_pre_value, type, value;
+            std::tie(c_pre_type, c_pre_value, ls, type, value) = e;
+            s << n << c_pre_type << c_pre_value << ls << type << value;
+        });
+}
+}
diff --git a/src/library/definitions_cache.h b/src/library/definitions_cache.h
new file mode 100644
index 0000000000..c573413e3c
--- /dev/null
+++ b/src/library/definitions_cache.h
@@ -0,0 +1,33 @@
+/*
+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 "util/name_map.h"
+#include "util/optional.h"
+#include "kernel/expr.h"
+
+namespace lean {
+/** \brief Cache for mapping definitions (type, value) before elaboration to (level_names, type, value)
+    after elaboration.
+*/
+class definitions_cache {
+    typedef std::tuple<expr, expr, level_param_names, expr, expr> entry;
+    name_map<entry> m_definitions;
+public:
+    definitions_cache();
+    definitions_cache(std::istream & in);
+    /** \brief Add the cache entry (n, pre_type, pre_value) -> (ls, type, value) */
+    void add(name const & n, expr const & pre_type, expr const & pre_value, level_param_names const & ls, expr const & type, expr const & value);
+    /** \brief Return (if available) elaborated (level_names, type, value) for (n, pre_type, pre_value).
+        The pre_type and pre_value are compared modulo placeholders names if the cached values.
+        In principle, we could have compared only the name and pre_type, but we only want to use cached values if the
+        user intent (captured by pre_value) did not change.
+    */
+    optional<std::tuple<level_param_names, expr, expr>> find(name const & n, expr const & pre_type, expr const & pre_value);
+    /** \brief Store the cache content into the given stream */
+    void save(std::ostream & out);
+};
+}
diff --git a/src/library/kernel_serializer.cpp b/src/library/kernel_serializer.cpp
index 0cab959107..fcfc4097c3 100644
--- a/src/library/kernel_serializer.cpp
+++ b/src/library/kernel_serializer.cpp
@@ -272,8 +272,8 @@ expr read_expr(deserializer & d) {
 }
 
 // Declaration serialization
-static serializer & operator<<(serializer & s, level_param_names const & ps) { return write_list<name>(s, ps); }
-static level_param_names read_level_params(deserializer & d) { return read_list<name>(d); }
+serializer & operator<<(serializer & s, level_param_names const & ps) { return write_list<name>(s, ps); }
+level_param_names read_level_params(deserializer & d) { return read_list<name>(d); }
 serializer & operator<<(serializer & s, declaration const & d) {
     char k = 0;
     if (d.is_definition()) {
diff --git a/src/library/kernel_serializer.h b/src/library/kernel_serializer.h
index 4ce48eee04..78dae8a539 100644
--- a/src/library/kernel_serializer.h
+++ b/src/library/kernel_serializer.h
@@ -18,6 +18,10 @@ inline deserializer & operator>>(deserializer & d, level & l) { l = read_level(d
 serializer & operator<<(serializer & s, levels const & ls);
 levels read_levels(deserializer & d);
 
+serializer & operator<<(serializer & s, level_param_names const & ps);
+level_param_names read_level_params(deserializer & d);
+inline deserializer & operator>>(deserializer & d, level_param_names & ps) { ps = read_level_params(d); return d; }
+
 serializer & operator<<(serializer & s, expr const & e);
 expr read_expr(deserializer & d);
 inline deserializer & operator>>(deserializer & d, expr & e) { e = read_expr(d); return d; }