diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean
index 83ade5de52..f7599fdf72 100644
--- a/library/init/meta/expr.lean
+++ b/library/init/meta/expr.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.meta.level init.control.monad
+import init.meta.level init.control.monad init.lean.expr
 universes u v
 
 structure pos :=
@@ -49,6 +49,7 @@ meta inductive expr
 | pi    : name → binder_info → expr → expr → expr
 | elet  : name → expr → expr → expr → expr
 | lit   : literal → expr
+| mdata : lean.kvmap → expr → expr
 | macro : macro_def → list expr → expr
 | quote : bool → expr → expr
 
@@ -339,6 +340,7 @@ meta def to_raw_fmt : expr → format
 | (lam n bi e t) := p ["lam", to_fmt n, repr bi, to_raw_fmt e, to_raw_fmt t]
 | (pi n bi e t) := p ["pi", to_fmt n, repr bi, to_raw_fmt e, to_raw_fmt t]
 | (elet n g e f) := p ["elet", to_fmt n, to_raw_fmt g, to_raw_fmt e, to_raw_fmt f]
+| (mdata d e) := p ["mdata", to_raw_fmt e]
 | (macro d args) := sbracket (format.join (list.intersperse " " ("macro" :: to_fmt (macro_def_name d) :: args.map to_raw_fmt)))
 | (quote b v) := p ["quote", to_fmt b, to_raw_fmt v]
 
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index b8abb589c0..f4ba235ef5 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -969,6 +969,7 @@ expr elaborator::visit_function(expr const & fn, bool has_args, optional<expr> c
     case expr_kind::FVar:      r = fn; break;
     case expr_kind::Constant:  r = visit_const_core(fn); break;
     case expr_kind::Macro:     r = visit_macro(fn, expected_type, true); break;
+    case expr_kind::MData:     r = visit_mdata(fn, expected_type); break;
     case expr_kind::Lambda:    r = visit_lambda(fn, expected_type); break;
     case expr_kind::Let:       r = visit_let(fn, expected_type); break;
     case expr_kind::Quote:
@@ -3354,6 +3355,11 @@ expr elaborator::visit_expr_quote(expr const & e, optional<expr> const & expecte
     return visit(q, expected_type);
 }
 
+expr elaborator::visit_mdata(expr const & e, optional<expr> const & expected_type) {
+    expr new_e = visit(mdata_expr(e), expected_type);
+    return update_mdata(e, new_e);
+}
+
 expr elaborator::visit_macro(expr const & e, optional<expr> const & expected_type, bool is_app_fn) {
     if (is_as_is(e)) {
         return get_as_is_arg(e);
@@ -3647,6 +3653,8 @@ expr elaborator::visit(expr const & e, optional<expr> const & expected_type) {
                         return e;
                     }
                     lean_unreachable();
+                case expr_kind::MData:
+                    return copy_pos(e, visit_mdata(e, expected_type));
                 case expr_kind::Sort:
                     return copy_pos(e, visit_sort(e));
                 case expr_kind::FVar:
diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h
index 1383a0532f..7c3bca76c3 100644
--- a/src/frontends/lean/elaborator.h
+++ b/src/frontends/lean/elaborator.h
@@ -236,6 +236,7 @@ private:
     expr visit_macro(expr const & e, optional<expr> const & expected_type, bool is_app_fn);
     expr visit_lambda(expr const & e, optional<expr> const & expected_type);
     expr visit_pi(expr const & e);
+    expr visit_mdata(expr const & e, optional<expr> const & expected_type);
     expr visit_app(expr const & e, optional<expr> const & expected_type);
     expr visit_let(expr const & e, optional<expr> const & expected_type);
     expr visit_convoy(expr const & e, optional<expr> const & expected_type);
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index ef2df50f87..6ef846c441 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -277,6 +277,8 @@ expr parser::copy_with_new_pos(expr const & e, pos_info p) {
     case expr_kind::Sort: case expr_kind::Constant: case expr_kind::MVar:
     case expr_kind::BVar: case expr_kind::FVar:     case expr_kind::Lit:
         return save_pos(copy(e), p);
+    case expr_kind::MData:
+        return save_pos(::lean::mk_mdata(mdata_data(e), copy_with_new_pos(mdata_expr(e), p)), p);
     case expr_kind::App:
         return save_pos(::lean::mk_app(copy_with_new_pos(app_fn(e), p),
                                        copy_with_new_pos(app_arg(e), p)),
@@ -1743,6 +1745,8 @@ static expr quote(expr const & e) {
         return mk_app(mk_constant({"expr", "const"}), quote(const_name(e)), mk_expr_placeholder());
     case expr_kind::MVar:
         return mk_expr_placeholder();
+    case expr_kind::MData:
+        throw exception("expr.mdata is not supported at quote function");
     case expr_kind::FVar:
         throw elaborator_exception(e, sstream() << "invalid quotation, unexpected local constant '"
                                    << mlocal_pp_name(e) << "'");
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index eebde51163..78c3668645 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -1784,6 +1784,7 @@ auto pretty_fn::pp(expr const & e, bool ignore_hide) -> result {
     case expr_kind::BVar:      return pp_var(e);
     case expr_kind::FVar:      return pp_local(e);
     case expr_kind::Sort:      return pp_sort(e);
+    case expr_kind::MData:     return pp(mdata_expr(e), ignore_hide);
     case expr_kind::Constant:  return pp_const(e);
     case expr_kind::MVar:      return pp_meta(e);
     case expr_kind::App:       return pp_app(e);
diff --git a/src/kernel/equiv_manager.cpp b/src/kernel/equiv_manager.cpp
index 7bbda82f58..aef6842497 100644
--- a/src/kernel/equiv_manager.cpp
+++ b/src/kernel/equiv_manager.cpp
@@ -95,6 +95,9 @@ bool equiv_manager::is_equiv_core(expr const & a, expr const & b) {
     case expr_kind::Lit:
         result = lit_value(a) == lit_value(b);
         break;
+    case expr_kind::MData:
+        result = mdata_expr(a) == mdata_expr(b);
+        break;
     case expr_kind::Let:
         result =
             is_equiv_core(let_type(a), let_type(b)) &&
diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index 4ac1ebb069..43b646378d 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -299,6 +299,26 @@ expr lit_type(expr_ptr e) {
     lean_unreachable();
 }
 
+// Expr metadata
+expr_mdata::expr_mdata(kvmap const & data, expr const & e):
+    expr_composite(expr_kind::MData, e.hash(),
+                   e.has_expr_metavar(),
+                   e.has_univ_metavar(),
+                   e.has_fvar(),
+                   e.has_param_univ(),
+                   inc_weight(get_weight(e)),
+                   get_loose_bvar_range(e)),
+    m_data(data), m_expr(e) {
+    m_depth = get_depth(e) + 1;
+    m_hash  = ::lean::hash(m_hash, m_weight);
+    m_hash  = ::lean::hash(m_hash, m_depth);
+}
+
+void expr_mdata::dealloc(buffer<expr_cell*> & todelete) {
+    dec_ref(m_expr,  todelete);
+    delete this;
+}
+
 // Let expressions
 expr_let::expr_let(name const & n, expr const & t, expr const & v, expr const & b):
     expr_composite(expr_kind::Let,
@@ -362,7 +382,9 @@ expr mk_metavar(name const & n, name const & pp_n, expr const & t) {
 expr mk_metavar(name const & n, expr const & t) {
     return mk_metavar(n, n, t);
 }
-
+expr mk_mdata(kvmap const & d, expr const & e) {
+    return expr(new expr_mdata(d, e));
+}
 expr mk_local(name const & n, name const & pp_n, expr const & t, binder_info const & bi) {
     return expr(new expr_fvar(n, pp_n, t, bi));
 }
@@ -398,6 +420,7 @@ void expr_cell::dealloc() {
             lean_assert(it->get_rc() == 0);
             switch (it->kind()) {
             case expr_kind::Lit:        static_cast<expr_lit*>(it)->dealloc(); break;
+            case expr_kind::MData:      static_cast<expr_mdata*>(it)->dealloc(todo); break;
             case expr_kind::BVar:       static_cast<expr_bvar*>(it)->dealloc(); break;
             case expr_kind::MVar:       static_cast<expr_mlocal*>(it)->dealloc(todo); break;
             case expr_kind::FVar:       static_cast<expr_fvar*>(it)->dealloc(todo); break;
@@ -527,6 +550,7 @@ unsigned get_weight(expr const & e) {
         return 1;
     case expr_kind::Lambda: case expr_kind::Pi:
     case expr_kind::App:    case expr_kind::Let:
+    case expr_kind::MData:
         return static_cast<expr_composite*>(e.raw())->m_weight;
 
 
@@ -545,6 +569,7 @@ unsigned get_depth(expr const & e) {
         return 1;
     case expr_kind::Lambda: case expr_kind::Pi:
     case expr_kind::App:    case expr_kind::Let:
+    case expr_kind::MData:
         return static_cast<expr_composite*>(e.raw())->m_depth;
 
 
@@ -556,6 +581,13 @@ unsigned get_depth(expr const & e) {
     lean_unreachable(); // LCOV_EXCL_LINE
 }
 
+expr update_mdata(expr const & e, expr const & t) {
+    if (!is_eqp(mdata_expr(e), t))
+        return mk_mdata(mdata_data(e), t);
+    else
+        return e;
+}
+
 expr update_app(expr const & e, expr const & new_fn, expr const & new_arg) {
     if (!is_eqp(app_fn(e), new_fn) || !is_eqp(app_arg(e), new_arg))
         return mk_app(new_fn, new_arg);
@@ -626,6 +658,7 @@ bool is_atomic(expr const & e) {
     case expr_kind::App:      case expr_kind::MVar:
     case expr_kind::FVar:     case expr_kind::Lambda:
     case expr_kind::Pi:       case expr_kind::Let:
+    case expr_kind::MData:
         return false;
 
 
@@ -779,6 +812,7 @@ unsigned hash_bi(expr const & e) {
 
 std::ostream & operator<<(std::ostream & out, expr_kind const & k) {
     switch (k) {
+    case expr_kind::MData:    out << "MData"; break;
     case expr_kind::Lit:      out << "Lit"; break;
     case expr_kind::BVar:     out << "BVar"; break;
     case expr_kind::FVar:     out << "FVar"; break;
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index d4bc42a4e3..7b19650228 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -19,6 +19,7 @@ Author: Leonardo de Moura
 #include "util/nat.h"
 #include "util/hash.h"
 #include "util/buffer.h"
+#include "util/kvmap.h"
 #include "util/list_fn.h"
 #include "util/sexpr/format.h"
 #include "kernel/level.h"
@@ -40,13 +41,14 @@ class expr;
           |   Pi            name expr expr
           |   Let           name expr expr expr
           |   Lit           literal
+          |   MData         kvmap expr
 
           The following constructors will be deleted in the future
 
           |   Quote         bool expr
           |   Macro         macro
 */
-enum class expr_kind { BVar, FVar, Sort, Constant, MVar, App, Lambda, Pi, Let, Lit, Macro, Quote };
+enum class expr_kind { BVar, FVar, Sort, Constant, MVar, App, Lambda, Pi, Let, Lit, MData, Macro, Quote };
 class expr_cell {
 protected:
     // The bits of the following field mean:
@@ -133,6 +135,7 @@ public:
     friend expr mk_binding(expr_kind k, name const & n, expr const & t, expr const & e, binder_info const & i);
     friend expr mk_let(name const & n, expr const & t, expr const & v, expr const & b);
     friend expr mk_lit(literal const & lit);
+    friend expr mk_mdata(kvmap const & m, expr const & e);
     friend bool is_eqp(expr const & a, expr const & b) { return a.m_ptr == b.m_ptr; }
 
     // TODO(Leo): delete
@@ -366,6 +369,18 @@ public:
     literal const & get_literal() const { return m_lit; }
 };
 
+class expr_mdata : public expr_composite {
+    kvmap m_data;
+    expr  m_expr;
+    friend expr_cell;
+    void dealloc(buffer<expr_cell*> & todelete);
+public:
+    expr_mdata(kvmap const & m, expr const & e);
+    ~expr_mdata() {}
+    kvmap const & get_data() const { return m_data; }
+    expr const & get_expr() const { return m_expr; }
+};
+
 // =======================================
 // Testers
 inline bool is_bvar(expr_ptr e)        { return e->kind() == expr_kind::BVar; }
@@ -378,6 +393,7 @@ inline bool is_pi(expr_ptr e)          { return e->kind() == expr_kind::Pi; }
 inline bool is_let(expr_ptr e)         { return e->kind() == expr_kind::Let; }
 inline bool is_sort(expr_ptr e)        { return e->kind() == expr_kind::Sort; }
 inline bool is_lit(expr_ptr e)         { return e->kind() == expr_kind::Lit; }
+inline bool is_mdata(expr_ptr e)       { return e->kind() == expr_kind::MData; }
 inline bool is_binding(expr_ptr e)     { return is_lambda(e) || is_pi(e); }
 
 bool is_atomic(expr const & e);
@@ -389,6 +405,7 @@ bool is_metavar_app(expr const & e);
 // =======================================
 // Constructors
 expr mk_lit(literal const & lit);
+expr mk_mdata(kvmap const & d, expr const & e);
 expr mk_bvar(unsigned idx);
 expr mk_fvar(name const & n);
 inline expr BVar(unsigned idx) { return mk_bvar(idx); }
@@ -449,6 +466,7 @@ inline expr mk_app(expr const & e1, expr const & e2, expr const & e3, expr const
 // =======================================
 // Casting (these functions are only needed for low-level code)
 inline expr_lit *         to_lit(expr_ptr e)        { lean_assert(is_lit(e));         return static_cast<expr_lit*>(e); }
+inline expr_mdata *       to_mdata(expr_ptr e)      { lean_assert(is_mdata(e));       return static_cast<expr_mdata*>(e); }
 inline expr_bvar *        to_bvar(expr_ptr e)       { lean_assert(is_bvar(e));        return static_cast<expr_bvar*>(e); }
 inline expr_fvar *        to_fvar(expr_ptr e)       { lean_assert(is_fvar(e));        return static_cast<expr_fvar*>(e); }
 inline expr_const *       to_constant(expr_ptr e)   { lean_assert(is_constant(e));    return static_cast<expr_const*>(e); }
@@ -466,6 +484,8 @@ inline unsigned        get_rc(expr_ptr e)                { return e->get_rc(); }
 inline bool            is_shared(expr_ptr e)             { return get_rc(e) > 1; }
 inline literal const & lit_value(expr_ptr e)             { return to_lit(e)->get_literal(); }
 expr lit_type(expr_ptr e);
+inline expr const &    mdata_expr(expr_ptr e)            { return to_mdata(e)->get_expr(); }
+inline kvmap const &   mdata_data(expr_ptr e)            { return to_mdata(e)->get_data(); }
 inline unsigned        bvar_idx(expr_ptr e)              { return to_bvar(e)->get_vidx(); }
 inline bool            is_bvar(expr_ptr e, unsigned i)   { return is_bvar(e) && bvar_idx(e) == i; }
 inline name const &    fvar_name(expr_ptr e)             { return to_fvar(e)->get_name(); }
@@ -555,6 +575,7 @@ expr update_local(expr const & e, binder_info const & bi);
 expr update_sort(expr const & e, level const & new_level);
 expr update_constant(expr const & e, levels const & new_levels);
 expr update_let(expr const & e, expr const & new_type, expr const & new_value, expr const & new_body);
+expr update_mdata(expr const & e, expr const & t);
 // =======================================
 
 
diff --git a/src/kernel/expr_eq_fn.cpp b/src/kernel/expr_eq_fn.cpp
index 815f442876..193bd1387c 100644
--- a/src/kernel/expr_eq_fn.cpp
+++ b/src/kernel/expr_eq_fn.cpp
@@ -72,6 +72,10 @@ class expr_eq_fn {
         switch (a.kind()) {
         case expr_kind::BVar:
             lean_unreachable(); // LCOV_EXCL_LINE
+        case expr_kind::MData:
+            return
+                apply(mdata_expr(a), mdata_expr(b)) &&
+                mdata_data(a) == mdata_data(b);
         case expr_kind::Lit:
             return lit_value(a) == lit_value(b);
         case expr_kind::Constant:
diff --git a/src/kernel/for_each_fn.cpp b/src/kernel/for_each_fn.cpp
index 2f6e72b423..eaa132f4cc 100644
--- a/src/kernel/for_each_fn.cpp
+++ b/src/kernel/for_each_fn.cpp
@@ -88,6 +88,9 @@ class for_each_fn {
             case expr_kind::Constant: case expr_kind::BVar:
             case expr_kind::Sort:     case expr_kind::Lit:
                 goto begin_loop;
+            case expr_kind::MData:
+                todo.emplace_back(mdata_expr(e), offset);
+                goto begin_loop;
             case expr_kind::FVar:
                 // TODO(Leo): delete after refactoring
                 todo.emplace_back(mlocal_type(e), offset);
diff --git a/src/kernel/old_type_checker.cpp b/src/kernel/old_type_checker.cpp
index 5fd6ca5bfd..9ef7f0eea6 100644
--- a/src/kernel/old_type_checker.cpp
+++ b/src/kernel/old_type_checker.cpp
@@ -225,6 +225,7 @@ expr old_type_checker::infer_type_core(expr const & e, bool infer_only) {
         if (!infer_only) check_level(sort_level(e));
         r = mk_sort(mk_succ(sort_level(e)));
         break;
+    case expr_kind::MData:     r = infer_type_core(mdata_expr(e), infer_only); break;
     case expr_kind::Constant:  r = infer_constant(e, infer_only);       break;
     case expr_kind::Macro:     r = infer_macro(e, infer_only);          break;
     case expr_kind::Lambda:    r = infer_lambda(e, infer_only);         break;
@@ -287,6 +288,8 @@ expr old_type_checker::whnf_core(expr const & e) {
     case expr_kind::BVar: case expr_kind::Sort:     case expr_kind::MVar:   case expr_kind::FVar:
     case expr_kind::Pi:   case expr_kind::Constant: case expr_kind::Lambda: case expr_kind::Lit:
         return e;
+    case expr_kind::MData:
+        return whnf_core(mdata_expr(e));
     case expr_kind::Macro: case expr_kind::App: case expr_kind::Let:
         break;
     case expr_kind::Quote: throw_found_quote(m_env);
@@ -304,6 +307,7 @@ expr old_type_checker::whnf_core(expr const & e) {
     switch (e.kind()) {
     case expr_kind::BVar:  case expr_kind::Sort:    case expr_kind::MVar:   case expr_kind::FVar:
     case expr_kind::Pi:   case expr_kind::Constant: case expr_kind::Lambda: case expr_kind::Lit:
+    case expr_kind::MData:
         lean_unreachable(); // LCOV_EXCL_LINE
     case expr_kind::Macro:
         if (auto m = expand_macro(e))
@@ -392,6 +396,8 @@ expr old_type_checker::whnf(expr const & e) {
     case expr_kind::BVar: case expr_kind::Sort: case expr_kind::MVar: case expr_kind::FVar:
     case expr_kind::Pi:   case expr_kind::Lit:
         return e;
+    case expr_kind::MData:
+        return whnf(mdata_expr(e));
     case expr_kind::Lambda:   case expr_kind::Macro: case expr_kind::App:
     case expr_kind::Constant: case expr_kind::Let:
         break;
@@ -482,6 +488,8 @@ lbool old_type_checker::quick_is_def_eq(expr const & t, expr const & s, bool use
         switch (t.kind()) {
         case expr_kind::Lambda: case expr_kind::Pi:
             return to_lbool(is_def_eq_binding(t, s));
+        case expr_kind::MData:
+            return to_lbool(is_def_eq(mdata_expr(t), mdata_expr(s)));
         case expr_kind::Sort:
             return to_lbool(is_def_eq(sort_level(t), sort_level(s)));
         case expr_kind::MVar:
diff --git a/src/kernel/replace_fn.cpp b/src/kernel/replace_fn.cpp
index 09a0bea2ea..15ba4206e9 100644
--- a/src/kernel/replace_fn.cpp
+++ b/src/kernel/replace_fn.cpp
@@ -82,6 +82,10 @@ class replace_rec_fn {
             case expr_kind::Constant: case expr_kind::Sort:
             case expr_kind::BVar:     case expr_kind::Lit:
                 return save_result(e, offset, e, shared);
+            case expr_kind::MData: {
+                expr new_e = apply(mdata_expr(e), offset);
+                return save_result(e, offset, update_mdata(e, new_e), shared);
+            }
             case expr_kind::MVar: {
                 expr new_t = apply(mlocal_type(e), offset);
                 return save_result(e, offset, update_mlocal(e, new_t), shared);
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index aaf30aeea5..8a9886c081 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -219,6 +219,7 @@ expr type_checker::infer_type_core(expr const & e, bool infer_only) {
     expr r;
     switch (e.kind()) {
     case expr_kind::Lit:       r = lit_type(e);    break;
+    case expr_kind::MData:     r = infer_type_core(mdata_expr(e), infer_only); break;
     case expr_kind::FVar:      r = infer_fvar(e);  break;
     case expr_kind::MVar:      r = mlocal_type(e); break;
     case expr_kind::BVar:
@@ -306,6 +307,8 @@ expr type_checker::whnf_core(expr const & e) {
     case expr_kind::Pi:   case expr_kind::Constant: case expr_kind::Lambda:
     case expr_kind::Lit:
         return e;
+    case expr_kind::MData:
+        return whnf_core(mdata_expr(e));
     case expr_kind::FVar:
         return whnf_fvar(e);
     case expr_kind::Macro: case expr_kind::App: case expr_kind::Let:
@@ -325,9 +328,9 @@ expr type_checker::whnf_core(expr const & e) {
     // do the actual work
     expr r;
     switch (e.kind()) {
-    case expr_kind::BVar:  case expr_kind::Sort:    case expr_kind::MVar: case expr_kind::FVar:
-    case expr_kind::Pi:   case expr_kind::Constant: case expr_kind::Lambda:
-    case expr_kind::Lit:
+    case expr_kind::BVar:  case expr_kind::Sort:     case expr_kind::MVar: case expr_kind::FVar:
+    case expr_kind::Pi:    case expr_kind::Constant: case expr_kind::Lambda:
+    case expr_kind::Lit:   case expr_kind::MData:
         lean_unreachable(); // LCOV_EXCL_LINE
 
     case expr_kind::Quote:
@@ -419,6 +422,8 @@ expr type_checker::whnf(expr const & e) {
     case expr_kind::BVar: case expr_kind::Sort: case expr_kind::MVar: case expr_kind::Pi:
     case expr_kind::Lit:
         return e;
+    case expr_kind::MData:
+        return whnf(mdata_expr(e));
     case expr_kind::FVar:
         return whnf_fvar(e);
     case expr_kind::Lambda:   case expr_kind::Macro: case expr_kind::App:
@@ -516,6 +521,8 @@ lbool type_checker::quick_is_def_eq(expr const & t, expr const & s, bool use_has
             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::MData:
+            return to_lbool(is_def_eq(mdata_expr(t), mdata_expr(s)));
         case expr_kind::MVar:
             lean_unreachable(); // LCOV_EXCL_LINE
         case expr_kind::BVar:      case expr_kind::FVar: case expr_kind::App:
diff --git a/src/library/check.cpp b/src/library/check.cpp
index 1164b9c964..f2fd296fce 100644
--- a/src/library/check.cpp
+++ b/src/library/check.cpp
@@ -125,6 +125,8 @@ struct check_fn {
             return visit_app(e);
         case expr_kind::Let:
             return visit_let(e);
+        case expr_kind::MData:
+            return visit(mdata_expr(e));
         case expr_kind::Macro:
             return visit_macro(e);
         case expr_kind::Quote:
diff --git a/src/library/compiler/cse.cpp b/src/library/compiler/cse.cpp
index f2feef9c10..5f1bba6010 100644
--- a/src/library/compiler/cse.cpp
+++ b/src/library/compiler/cse.cpp
@@ -57,6 +57,7 @@ class cse_fn : public compiler_step_visitor {
             case expr_kind::Macro:    visit_macro(e); break;
             case expr_kind::App:      visit_app(e); break;
             case expr_kind::Let:      visit_let(e); break;
+            case expr_kind::MData:    visit(mdata_expr(e)); break;
             case expr_kind::Quote:
                 break;
             }
diff --git a/src/library/compiler/vm_compiler.cpp b/src/library/compiler/vm_compiler.cpp
index c2321ba899..d39a469a14 100644
--- a/src/library/compiler/vm_compiler.cpp
+++ b/src/library/compiler/vm_compiler.cpp
@@ -310,6 +310,7 @@ class vm_compiler_fn {
         case expr_kind::Pi:       lean_unreachable();
         case expr_kind::Lambda:   lean_unreachable();
         case expr_kind::Macro:    compile_macro(e, bpz, m);  break;
+        case expr_kind::MData:    compile(mdata_expr(e), bpz, m); break;
         case expr_kind::Constant: compile_constant(e);       break;
         case expr_kind::FVar:     compile_local(e, m);       break;
         case expr_kind::App:      compile_app(e, bpz, m);    break;
diff --git a/src/library/deep_copy.cpp b/src/library/deep_copy.cpp
index 7bb3cb158e..655bd633a2 100644
--- a/src/library/deep_copy.cpp
+++ b/src/library/deep_copy.cpp
@@ -12,6 +12,7 @@ namespace lean {
 expr copy(expr const & a) {
     switch (a.kind()) {
     case expr_kind::Lit:      return mk_lit(lit_value(a));
+    case expr_kind::MData:    return mk_mdata(mdata_data(a), mdata_expr(a));
     case expr_kind::BVar:     return mk_var(var_idx(a));
     case expr_kind::FVar:     return mk_local(mlocal_name(a), mlocal_pp_name(a), mlocal_type(a), local_info(a));
     case expr_kind::Constant: return mk_constant(const_name(a), const_levels(a));
diff --git a/src/library/equations_compiler/structural_rec.cpp b/src/library/equations_compiler/structural_rec.cpp
index 43f947d63a..e879f469ed 100644
--- a/src/library/equations_compiler/structural_rec.cpp
+++ b/src/library/equations_compiler/structural_rec.cpp
@@ -151,6 +151,8 @@ struct structural_rec_fn {
                 }
                 return true;
             }
+            case expr_kind::MData:
+                return check_rhs(mdata_expr(e));
             case expr_kind::Let:
                 if (!check_rhs(let_value(e))) {
                     return false;
diff --git a/src/library/expr_lt.cpp b/src/library/expr_lt.cpp
index e353a7b851..65b73db911 100644
--- a/src/library/expr_lt.cpp
+++ b/src/library/expr_lt.cpp
@@ -25,6 +25,11 @@ bool is_lt(expr const & a, expr const & b, bool use_hash, local_context const *
         return lit_value(a) < lit_value(b);
     case expr_kind::BVar:
         return var_idx(a) < var_idx(b);
+    case expr_kind::MData:
+        if (mdata_expr(a) != mdata_expr(b))
+            return is_lt(mdata_expr(a), mdata_expr(b), use_hash, lctx);
+        else
+            return mdata_data(a) < mdata_data(b);
     case expr_kind::Constant:
         if (const_name(a) != const_name(b))
             return const_name(a) < const_name(b);
@@ -136,6 +141,11 @@ bool is_lt_no_level_params(expr const & a, expr const & b) {
         return lit_value(a) < lit_value(b);
     case expr_kind::BVar:
         return var_idx(a) < var_idx(b);
+    case expr_kind::MData:
+        if (mdata_expr(a) != mdata_expr(b))
+            return is_lt_no_level_params(mdata_expr(a), mdata_expr(b));
+        else
+            return mdata_data(a) < mdata_data(b);
     case expr_kind::Constant:
         if (const_name(a) != const_name(b))
             return const_name(a) < const_name(b);
diff --git a/src/library/inductive_compiler/nested.cpp b/src/library/inductive_compiler/nested.cpp
index 0cfe9755e1..0814133434 100644
--- a/src/library/inductive_compiler/nested.cpp
+++ b/src/library/inductive_compiler/nested.cpp
@@ -534,6 +534,7 @@ class add_nested_inductive_decl_fn {
         case expr_kind::Macro:
         case expr_kind::Quote:
         case expr_kind::Lit:
+        case expr_kind::MData:
             return _e;
         case expr_kind::Lambda:
         case expr_kind::Pi:
@@ -590,6 +591,7 @@ class add_nested_inductive_decl_fn {
         case expr_kind::Macro:
         case expr_kind::Quote:
         case expr_kind::Lit:
+        case expr_kind::MData:
             return _e;
         case expr_kind::Lambda:
         case expr_kind::Pi:
diff --git a/src/library/kernel_serializer.cpp b/src/library/kernel_serializer.cpp
index a909654b9e..05ee7126c5 100644
--- a/src/library/kernel_serializer.cpp
+++ b/src/library/kernel_serializer.cpp
@@ -61,6 +61,10 @@ class expr_serializer : public object_serializer<expr, expr_hash, is_bi_equal_pr
                 case expr_kind::Lit:
                     s << lit_value(a);
                     break;
+                case expr_kind::MData:
+                    s << mdata_data(a);
+                    write_core(mdata_expr(a));
+                    break;
                 case expr_kind::Constant:
                     lean_assert(!const_name(a).is_anonymous());
                     s << const_name(a) << const_levels(a);
@@ -131,6 +135,10 @@ public:
                     return mk_var(d.read_unsigned());
                 case expr_kind::Lit:
                     return mk_lit(read_literal(d));
+                case expr_kind::MData: {
+                    kvmap m = read_list_ref<pair_ref<name, data_value>>(d);
+                    return mk_mdata(m, read());
+                }
                 case expr_kind::Constant: {
                     auto n = read_name(d);
                     return mk_constant(n, read_levels(d));
diff --git a/src/library/locals.cpp b/src/library/locals.cpp
index f3a727bdd7..d64c07652e 100644
--- a/src/library/locals.cpp
+++ b/src/library/locals.cpp
@@ -75,6 +75,9 @@ void collect_locals(expr const & e, collected_locals & ls, bool restricted) {
         case expr_kind::BVar: case expr_kind::Constant:
         case expr_kind::Sort: case expr_kind::Lit:
             break; // do nothing
+        case expr_kind::MData:
+            visit(mdata_expr(e));
+            break;
         case expr_kind::FVar:
             if (!restricted)
                 visit(mlocal_type(e));
diff --git a/src/library/max_sharing.cpp b/src/library/max_sharing.cpp
index efca5118d9..615d333929 100644
--- a/src/library/max_sharing.cpp
+++ b/src/library/max_sharing.cpp
@@ -62,10 +62,15 @@ struct max_sharing_fn::imp {
         case expr_kind::Sort:
             res = update_sort(a, apply(sort_level(a)));
             break;
+        case expr_kind::MData: {
+            expr new_e = apply(mdata_expr(a));
+            res = update_mdata(a, new_e);
+            break;
+        }
         case expr_kind::App: {
             expr new_f = apply(app_fn(a));
             expr new_a = apply(app_arg(a));
-                res = update_app(a, new_f, new_a);
+            res = update_app(a, new_f, new_a);
             break;
         }
         case expr_kind::Lambda: case expr_kind::Pi: {
diff --git a/src/library/noncomputable.cpp b/src/library/noncomputable.cpp
index 2ebec0dbf3..d38b8be3b5 100644
--- a/src/library/noncomputable.cpp
+++ b/src/library/noncomputable.cpp
@@ -200,6 +200,7 @@ struct get_noncomputable_reason_fn {
         case expr_kind::Lambda:    visit_binding(e);  return;
         case expr_kind::Pi:        visit_binding(e);  return;
         case expr_kind::Let:       visit_let(e);      return;
+        case expr_kind::MData:     visit(mdata_expr(e)); return;
         case expr_kind::Quote:     return;
         }
     }
diff --git a/src/library/normalize.cpp b/src/library/normalize.cpp
index 014db3c472..86f13dddef 100644
--- a/src/library/normalize.cpp
+++ b/src/library/normalize.cpp
@@ -119,6 +119,8 @@ class normalize_fn {
         case expr_kind::BVar: case expr_kind::Constant: case expr_kind::Sort:
         case expr_kind::MVar: case expr_kind::FVar:     case expr_kind::Lit:
             return e;
+        case expr_kind::MData:
+            lean_unreachable();
         case expr_kind::Lambda: {
             e = normalize_binding(e);
             if (m_use_eta)
diff --git a/src/library/pos_info_provider.cpp b/src/library/pos_info_provider.cpp
index f7d25ace2c..54a237a885 100644
--- a/src/library/pos_info_provider.cpp
+++ b/src/library/pos_info_provider.cpp
@@ -143,6 +143,10 @@ class replace_rec_fn2 {
                 expr new_t = apply(mlocal_type(e), offset);
                 return save_result(e, offset, copy_pos(e, update_mlocal(e, new_t)), shared);
             }
+            case expr_kind::MData: {
+                expr new_e = apply(mdata_expr(e), offset);
+                return save_result(e, offset, copy_pos(e, update_mdata(e, new_e)), shared);
+            }
             case expr_kind::App: {
                 expr new_f = apply(app_fn(e), offset);
                 expr new_a = apply(app_arg(e), offset);
diff --git a/src/library/print.cpp b/src/library/print.cpp
index 56b91386c5..78b85418b4 100644
--- a/src/library/print.cpp
+++ b/src/library/print.cpp
@@ -222,6 +222,9 @@ struct print_expr_fn {
         case expr_kind::FVar:
             out() << fix_name(mlocal_pp_name(a));
             break;
+        case expr_kind::MData:
+            out() << "[mdata "; print(mdata_expr(a)); out() << "]";
+            break;
         case expr_kind::BVar:
             out() << "#" << var_idx(a);
             break;
diff --git a/src/library/replace_visitor.cpp b/src/library/replace_visitor.cpp
index 9f4613bc73..2b74ff61d8 100644
--- a/src/library/replace_visitor.cpp
+++ b/src/library/replace_visitor.cpp
@@ -24,6 +24,7 @@ expr replace_visitor::visit_mlocal(expr const & e) {
 }
 expr replace_visitor::visit_meta(expr const & e) { return visit_mlocal(e); }
 expr replace_visitor::visit_local(expr const & e) { return visit_mlocal(e); }
+expr replace_visitor::visit_mdata(expr const & e) { return visit(mdata_expr(e)); }
 expr replace_visitor::visit_app(expr const & e) {
     lean_assert(is_app(e));
     expr new_fn  = visit(app_fn(e));
@@ -69,6 +70,7 @@ expr replace_visitor::visit(expr const & e) {
 
     switch (e.kind()) {
     case expr_kind::Lit:       return save_result(e, visit_lit(e), shared);
+    case expr_kind::MData:     return save_result(e, visit_mdata(e), shared);
     case expr_kind::Sort:      return save_result(e, visit_sort(e), shared);
     case expr_kind::Constant:  return save_result(e, visit_constant(e), shared);
     case expr_kind::BVar:      return save_result(e, visit_var(e), shared);
diff --git a/src/library/replace_visitor.h b/src/library/replace_visitor.h
index 9f7ba24217..b0cb3d1f19 100644
--- a/src/library/replace_visitor.h
+++ b/src/library/replace_visitor.h
@@ -30,6 +30,7 @@ protected:
     virtual expr visit_pi(expr const &);
     virtual expr visit_let(expr const & e);
     virtual expr visit_lit(expr const & e);
+    virtual expr visit_mdata(expr const & e);
     virtual expr visit(expr const &);
 
     virtual expr visit_macro(expr const &);
diff --git a/src/library/tactic/dsimplify.cpp b/src/library/tactic/dsimplify.cpp
index 4a9c0ee1ab..0ef041e9b8 100644
--- a/src/library/tactic/dsimplify.cpp
+++ b/src/library/tactic/dsimplify.cpp
@@ -260,6 +260,9 @@ expr dsimplify_core_fn::visit(expr const & e) {
         case expr_kind::Constant:
             new_e = curr_e;
             break;
+        case expr_kind::MData:
+            new_e = mdata_expr(curr_e);
+            break;
         case expr_kind::BVar:
             lean_unreachable();
         case expr_kind::MVar:
diff --git a/src/library/tactic/simp_lemmas.cpp b/src/library/tactic/simp_lemmas.cpp
index 7e3ed5f505..420d6567e4 100644
--- a/src/library/tactic/simp_lemmas.cpp
+++ b/src/library/tactic/simp_lemmas.cpp
@@ -645,6 +645,8 @@ static bool is_permutation(expr const & lhs, expr const & rhs, unsigned offset,
         } else {
             return lhs == rhs; // free variable
         }
+    case expr_kind::MData:
+        return is_permutation(mdata_expr(lhs), mdata_expr(rhs), offset, p);
     case expr_kind::Lambda: case expr_kind::Pi:
         return
             is_permutation(binding_domain(lhs), binding_domain(rhs), offset, p) &&
diff --git a/src/library/tactic/simplify.cpp b/src/library/tactic/simplify.cpp
index 5f576204b3..7efcc6fa9f 100644
--- a/src/library/tactic/simplify.cpp
+++ b/src/library/tactic/simplify.cpp
@@ -668,7 +668,9 @@ simp_result simplify_core_fn::visit(expr const & e, optional<expr> const & paren
         case expr_kind::Let:
             new_result = join(curr_result, visit_let(curr_result.get_new()));
             break;
-
+        case expr_kind::MData:
+            new_result = join(curr_result, visit(mdata_expr(e), some_expr(e)));
+            break;
         case expr_kind::Macro:
             new_result = join(curr_result, visit_macro(curr_result.get_new()));
             break;
diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index 5e9b4eb203..15d93ad69d 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -790,6 +790,9 @@ expr type_context_old::whnf_core(expr const & e0, bool proj_reduce) {
     case expr_kind::Constant: case expr_kind::Lit:
         /* Remark: we do not unfold Constants eagerly in this method */
         return e;
+    case expr_kind::MData:
+        e = mdata_expr(e);
+        continue;
     case expr_kind::FVar:
         if (use_zeta() && is_local_decl_ref(e)) {
             if (auto d = m_lctx.find_local_decl(e)) {
@@ -1010,6 +1013,9 @@ expr type_context_old::infer_core(expr const & e) {
     case expr_kind::MVar:
         r = infer_metavar(e);
         break;
+    case expr_kind::MData:
+        r = infer_core(mdata_expr(e));
+        break;
     case expr_kind::BVar:
         throw exception("failed to infer type, unexpected bound variable occurrence");
     case expr_kind::Sort:
@@ -2717,6 +2723,8 @@ lbool type_context_old::quick_is_def_eq(expr const & e1, expr const & e2) {
             return to_lbool(is_def_eq_binding(e1, e2));
         case expr_kind::Sort:
             return to_lbool(is_def_eq(sort_level(e1), sort_level(e2)));
+        case expr_kind::MData:
+            return to_lbool(is_def_eq_core(mdata_expr(e1), mdata_expr(e2)));
         case expr_kind::Lit:
             return to_lbool(lit_value(e1) == lit_value(e2));
         case expr_kind::MVar:     case expr_kind::BVar:
@@ -3378,6 +3386,9 @@ lbool type_context_old::is_quick_class(expr const & type, name & result) {
         case expr_kind::Pi:
             it = &binding_body(*it);
             break;
+        case expr_kind::MData:
+            it = &mdata_expr(*it);
+            break;
         case expr_kind::Macro:
             return l_undef;
         case expr_kind::Quote:
diff --git a/src/library/vm/vm_expr.cpp b/src/library/vm/vm_expr.cpp
index e9a480d930..d5a0064328 100644
--- a/src/library/vm/vm_expr.cpp
+++ b/src/library/vm/vm_expr.cpp
@@ -167,6 +167,31 @@ vm_obj expr_macro_def_name(vm_obj const & d) {
     return to_obj(to_macro_definition(d).get_name());
 }
 
+/*
+inductive data_value
+| of_string (v : string)
+| of_nat    (v : nat)
+| of_bool   (v : bool)
+| of_name   (v : name)
+*/
+vm_obj to_obj(data_value const & d) {
+    switch (d.kind()) {
+    case data_value_kind::String: return mk_vm_constructor(0, to_obj(d.get_string().to_std_string()));
+    case data_value_kind::Nat:    return mk_vm_constructor(1, mk_vm_nat(d.get_nat().to_mpz()));
+    case data_value_kind::Bool:   return mk_vm_constructor(2, mk_vm_bool(d.get_bool()));
+    case data_value_kind::Name:   return mk_vm_constructor(3, to_obj(d.get_name()));
+    }
+    lean_unreachable();
+}
+
+vm_obj to_obj(kvmap const & m) {
+    buffer<vm_obj> objs;
+    for (pair_ref<name, data_value> const & p : m) {
+        objs.push_back(mk_vm_pair(to_obj(p.fst()), to_obj(p.snd())));
+    }
+    return to_obj(objs);
+}
+
 unsigned expr_cases_on(vm_obj const & o, buffer<vm_obj> & data) {
     expr const & e = to_expr(o);
     switch (e.kind()) {
@@ -215,6 +240,10 @@ unsigned expr_cases_on(vm_obj const & o, buffer<vm_obj> & data) {
             break;
         }
         break;
+    case expr_kind::MData:
+        data.push_back(to_obj(mdata_data(e)));
+        data.push_back(to_obj(mdata_expr(e)));
+        break;
     case expr_kind::Macro: {
         data.push_back(to_obj(macro_def(e)));
         buffer<expr> args;
diff --git a/src/util/list_ref.h b/src/util/list_ref.h
index b13e607345..fe391767f8 100644
--- a/src/util/list_ref.h
+++ b/src/util/list_ref.h
@@ -77,7 +77,7 @@ public:
             T const & h2 = ::lean::head<T>(it2);
             if (h1 < h2)
                 return true;
-            if (h2 > h1)
+            if (h2 < h1)
                 return false;
             it1 = cnstr_obj(it1, 1);
             it2 = cnstr_obj(it2, 1);