diff --git a/src/library/definitional/init_module.cpp b/src/library/definitional/init_module.cpp
index fd527cbad1..b8607c95b1 100644
--- a/src/library/definitional/init_module.cpp
+++ b/src/library/definitional/init_module.cpp
@@ -6,13 +6,16 @@ Author: Leonardo de Moura
 */
 #include "library/util.h"
 #include "library/definitional/equations.h"
+#include "library/definitional/projection.h"
 
 namespace lean{
 void initialize_definitional_module() {
     initialize_equations();
+    initialize_def_projection();
 }
 
 void finalize_definitional_module() {
+    finalize_def_projection();
     finalize_equations();
 }
 }
diff --git a/src/library/definitional/projection.cpp b/src/library/definitional/projection.cpp
index b2f5093c05..f1583ae0eb 100644
--- a/src/library/definitional/projection.cpp
+++ b/src/library/definitional/projection.cpp
@@ -16,6 +16,7 @@ Author: Leonardo de Moura
 #include "library/module.h"
 #include "library/util.h"
 #include "library/normalize.h"
+#include "library/kernel_serializer.h"
 #include "library/definitional/projection.h"
 
 namespace lean {
@@ -51,6 +52,130 @@ static bool is_prop(expr type) {
     return is_sort(type) && is_zero(sort_level(type));
 }
 
+
+static name * g_projection_macro_name    = nullptr;
+static std::string * g_projection_opcode = nullptr;
+
+/** \brief Auxiliary macro used to implement projections efficiently.
+    They bypass the recursor.
+
+    These macros are only used to speedup type checking when sending declarations to the kernel.
+    During elaboration, we use a custom converter that never unfolds projections.
+*/
+class projection_macro_definition_cell : public macro_definition_cell {
+    name              m_I_name;
+    name              m_constructor_name;
+    name              m_proj_name;
+    unsigned          m_idx;
+    level_param_names m_ps;
+    expr              m_type;
+    expr              m_val; // expanded form
+    void check_macro(expr const & m) const {
+        if (!is_macro(m) || macro_num_args(m) != 1)
+            throw exception(sstream() << "invalid '" << m_proj_name
+                            << "' projection macro, incorrect number of arguments");
+    }
+
+public:
+    projection_macro_definition_cell(name const & I, name const & c, name const & p, unsigned i,
+                                     level_param_names const & ps, expr const & type, expr const & val):
+        m_I_name(I), m_constructor_name(c), m_proj_name(p), m_idx(i), m_ps(ps), m_type(type), m_val(val) {}
+
+    virtual name get_name() const { return m_proj_name; }
+    virtual format pp(formatter const &) const { return format(m_proj_name); }
+    virtual void display(std::ostream & out) const { out << m_proj_name; }
+    virtual pair<expr, constraint_seq> check_type(expr const & m, extension_context & ctx, bool infer_only) const {
+        check_macro(m);
+        environment const & env = ctx.env();
+        constraint_seq cs;
+        expr s   = macro_arg(m, 0);
+        expr s_t = ctx.whnf(ctx.check_type(s, cs, infer_only), cs);
+        buffer<expr> I_args;
+        expr const & I = get_app_args(s_t, I_args);
+        if (!is_constant(I)) {
+            // remark: this is not an issue since this macro should not be used during elaboration.
+            throw_kernel_exception(env, sstream() << "projection macros do not support arbitrary terms "
+                                   << "containing metavariables yet (solution: use trust-level 0)", m);
+        }
+
+        if (length(const_levels(I)) != length(m_ps))
+            throw_kernel_exception(env, sstream() << "invalid projection application '" << m_proj_name
+                                   << "', incorrect number of universe parameters", m);
+        expr t = instantiate_univ_params(m_type, m_ps, const_levels(I));
+        I_args.push_back(s);
+        return mk_pair(instantiate_rev(t, I_args.size(), I_args.data()), cs);
+    }
+
+    virtual optional<expr> expand(expr const & m, extension_context & ctx) const {
+        check_macro(m);
+        expr const & s  = macro_arg(m, 0);
+        constraint_seq cs;
+        expr new_s      = ctx.whnf(s, cs);
+        if (cs)
+            return none_expr();
+        buffer<expr> c_args;
+        expr const & c  = get_app_args(new_s, c_args);
+        if (is_constant(c) && const_name(c) == m_constructor_name && m_idx < c_args.size()) {
+            return some_expr(c_args[m_idx]);
+        } else {
+            // expand into recursor
+            expr s_type = ctx.whnf(ctx.infer_type(s, cs), cs);
+            if (cs)
+                return none_expr();
+            buffer<expr> args;
+            expr const & I = get_app_args(s_type, args);
+            if (!is_constant(I) || length(m_ps) != length(const_levels(I)))
+                return none_expr();
+            expr r = instantiate_univ_params(m_val, m_ps, const_levels(I));
+            args.push_back(new_s);
+            return some(instantiate_rev(r, args.size(), args.data()));
+        }
+    }
+
+    virtual void write(serializer & s) const {
+        s.write_string(*g_projection_opcode);
+        s << m_I_name << m_constructor_name << m_proj_name << m_idx << m_ps << m_type << m_val;
+    }
+
+    virtual bool operator==(macro_definition_cell const & other) const {
+        if (auto other_ptr = dynamic_cast<projection_macro_definition_cell const *>(&other)) {
+            return m_proj_name == other_ptr->m_proj_name;
+        } else {
+            return false;
+        }
+    }
+
+    virtual unsigned hash() const {
+        return m_proj_name.hash();
+    }
+};
+
+static expr mk_projection_macro(name const & I, name const & c, name const & p, unsigned i,
+                                level_param_names const & ps, expr const & type, expr const & val, expr const & arg) {
+    macro_definition m(new projection_macro_definition_cell(I, c, p, i, ps, type, val));
+    return mk_macro(m, 1, &arg);
+}
+
+void initialize_def_projection() {
+    g_projection_macro_name = new name("projection");
+    g_projection_opcode     = new std::string("Proj");
+    register_macro_deserializer(*g_projection_opcode,
+                                [](deserializer & d, unsigned num, expr const * args) {
+                                    if (num != 1)
+                                        throw corrupted_stream_exception();
+                                    name I_name, c_name, proj_name; unsigned idx;
+                                    level_param_names ps; expr type, val;
+                                    d >> I_name >> c_name >> proj_name >> idx >> ps >> type >> val;
+                                    return mk_projection_macro(I_name, c_name, proj_name, idx,
+                                                               ps, type, val, args[0]);
+                                });
+}
+
+void finalize_def_projection() {
+    delete g_projection_macro_name;
+    delete g_projection_opcode;
+}
+
 environment mk_projections(environment const & env, name const & n, buffer<name> const & proj_names,
                            implicit_infer_kind infer_k, bool inst_implicit) {
     // Given an inductive datatype C A (where A represent parameters)
@@ -116,6 +241,18 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
         expr proj_type    = Pi(proj_args, result_type);
         proj_type         = infer_implicit_params(proj_type, nparams, infer_k);
         expr proj_val     = Fun(proj_args, rec_app);
+        if (new_env.trust_lvl() > 0) {
+            // use macros
+            expr mval  = proj_val;
+            expr mtype = proj_type;
+            for (unsigned i = 0; i < proj_args.size(); i++) {
+                mval  = binding_body(mval);
+                mtype = binding_body(mtype);
+            }
+            proj_val = mk_projection_macro(n, inductive::intro_rule_name(intro), proj_name,
+                                           nparams + i, lvl_params, mtype, mval, proj_args.back());
+            proj_val = Fun(proj_args, proj_val);
+        }
         bool use_conv_opt = false;
         declaration new_d = mk_definition(env, proj_name, lvl_params, proj_type, proj_val,
                                           use_conv_opt);
diff --git a/src/library/definitional/projection.h b/src/library/definitional/projection.h
index b34d6205ec..4194b3722c 100644
--- a/src/library/definitional/projection.h
+++ b/src/library/definitional/projection.h
@@ -22,4 +22,7 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
                            implicit_infer_kind infer_k = implicit_infer_kind::Implicit, bool inst_implicit = false);
 environment mk_projections(environment const & env, name const & n,
                            implicit_infer_kind infer_k = implicit_infer_kind::Implicit, bool inst_implicit = false);
+
+void initialize_def_projection();
+void finalize_def_projection();
 }