diff --git a/src/library/equations_compiler/compiler.cpp b/src/library/equations_compiler/compiler.cpp
index f114473928..4b0bf79eaf 100644
--- a/src/library/equations_compiler/compiler.cpp
+++ b/src/library/equations_compiler/compiler.cpp
@@ -15,7 +15,7 @@ Author: Leonardo de Moura
 namespace lean {
 #define trace_compiler(Code) lean_trace("eqn_compiler", scope_trace_env _scope1(ctx->env(), ctx); Code)
 
-expr compile_equations(environment const & env, options const & opts, metavar_context & mctx, local_context const & lctx,
+expr compile_equations(environment & env, options const & opts, metavar_context & mctx, local_context const & lctx,
                        expr const & eqns) {
     aux_type_context ctx(env, opts, mctx, lctx, transparency_mode::Semireducible);
     trace_compiler(tout() << "compiling\n" << eqns << "\n";);
@@ -28,7 +28,7 @@ expr compile_equations(environment const & env, options const & opts, metavar_co
     unsigned arg_idx;
     optional<expr> eqns1 = try_structural_rec(ctx.get(), eqns, arg_idx);
     if (eqns1) {
-        elim_match(ctx.get(), eqns);
+        elim_match(env, opts, mctx, lctx, *eqns1);
     }
 
     // test unbounded_rec
diff --git a/src/library/equations_compiler/compiler.h b/src/library/equations_compiler/compiler.h
index c80bf555b3..3d25a0f285 100644
--- a/src/library/equations_compiler/compiler.h
+++ b/src/library/equations_compiler/compiler.h
@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include "library/metavar_context.h"
 #include "library/equations_compiler/equations.h"
 namespace lean {
-expr compile_equations(environment const & env, options const & opts, metavar_context & mctx, local_context const & lctx,
+expr compile_equations(environment & env, options const & opts, metavar_context & mctx, local_context const & lctx,
                        expr const & eqns);
 void initialize_compiler();
 void finalize_compiler();
diff --git a/src/library/equations_compiler/elim_match.cpp b/src/library/equations_compiler/elim_match.cpp
index 7d0c7014e8..a9ade38ba1 100644
--- a/src/library/equations_compiler/elim_match.cpp
+++ b/src/library/equations_compiler/elim_match.cpp
@@ -4,40 +4,144 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "kernel/instantiate.h"
 #include "library/trace.h"
+#include "library/tactic/tactic_state.h"
+#include "library/tactic/cases_tactic.h"
 #include "library/equations_compiler/equations.h"
 #include "library/equations_compiler/util.h"
 
 namespace lean {
-#define trace_match(Code) lean_trace(name({"eqn_compiler", "elim_match"}), scope_trace_env _scope1(m_ctx.env(), m_ctx); Code)
-
+// #define trace_match(Code) lean_trace(name({"eqn_compiler", "elim_match"}), scope_trace_env _scope1(m_ctx.env(), m_ctx); Code)
 struct elim_match_fn {
-    type_context & m_ctx;
-    elim_match_fn(type_context & ctx):m_ctx(ctx) {}
+    environment     m_env;
+    options         m_opts;
+    metavar_context m_mctx;
+
+    elim_match_fn(environment const & env, options const & opts,
+                  metavar_context const & mctx):
+        m_env(env), m_opts(opts), m_mctx(mctx) {}
 
     struct equation {
-        list<expr> m_vars;
-        list<expr> m_patterns;
-        expr       m_rhs;
+        list<pair<name, name>> m_renames;
+        local_context          m_lctx;
+        list<expr>             m_patterns;
+        expr                   m_rhs;
+        expr                   m_ref; /* for reporting errors */
+        unsigned               m_idx;
     };
 
     struct program {
+        /* Metavariable containing the context for the program */
+        expr           m_goal;
         /* Variables that still need to be matched/processed */
-        list<expr> m_var_stack;
-        list<expr> m_equations;
+        list<name>     m_var_stack;
+        list<equation> m_equations;
     };
 
+    type_context mk_type_context(local_context const & lctx) {
+        return mk_type_context_for(m_env, m_opts, m_mctx, lctx);
+    }
 
-    pair<expr, environment> operator()(expr const & e) {
-        unpack_eqns ues(m_ctx, e);
-        lean_assert(ues.get_num_fns() == 1);
+    unsigned get_arity(local_context const & lctx, expr const & e) {
+        /* Naive way to retrieve the arity of the function being defined */
+        lean_assert(is_equations(e));
+        type_context ctx = mk_type_context(lctx);
+        unpack_eqns ues(ctx, e);
+        return ues.get_arity_of(0);
+    }
+
+    pair<expr, list<name>>
+    mk_main_goal(local_context lctx, expr fn_type, unsigned arity) {
+        type_context ctx = mk_type_context(lctx);
+        buffer<name> vars;
+        name x("_x");
+        for (unsigned i = 0; i < arity; i++) {
+            fn_type = ctx.whnf(fn_type);
+            if (!is_pi(fn_type)) throw_ill_formed_eqns();
+            expr var = ctx.push_local(x.append_after(i+1), binding_domain(fn_type));
+            vars.push_back(mlocal_name(var));
+            fn_type  = instantiate(binding_body(fn_type), var);
+        }
+        m_mctx = ctx.mctx();
+        expr m = m_mctx.mk_metavar_decl(ctx.lctx(), fn_type);
+        return mk_pair(m, to_list(vars));
+    }
+
+    optional<equation> mk_equation(local_context const & lctx, expr const & eqn, unsigned idx) {
+        expr it = eqn;
+        it = binding_body(it); /* consume fn header */
+        if (is_no_equation(it)) return optional<equation>();
+        type_context ctx = mk_type_context(lctx);
+        buffer<expr> locals;
+        while (is_lambda(it)) {
+            expr type  = instantiate_rev(binding_domain(it), locals);
+            expr local = ctx.push_local(binding_name(it), type);
+            locals.push_back(local);
+            it = binding_body(it);
+        }
+        lean_assert(is_equation(it));
+        equation E;
+        E.m_lctx = ctx.lctx();
+        E.m_rhs  = instantiate_rev(equation_rhs(it), locals);
+        /* The function being defined is not recursive. So, E.m_rhs
+           must be closed even if we "consumed" the fn header in
+           the beginning of the method. */
+        lean_assert(closed(E.m_rhs));
+        buffer<expr> patterns;
+        get_app_args(equation_lhs(it), patterns);
+        for (expr & p : patterns) {
+            p = instantiate_rev(p, patterns);
+        }
+        E.m_patterns = to_list(patterns);
+        E.m_ref  = eqn;
+        E.m_idx  = idx;
+        return optional<equation>(E);
+    }
+
+    list<equation> mk_equations(local_context const & lctx, buffer<expr> const & eqns) {
+        buffer<equation> R;
+        unsigned idx = 0;
+        for (expr const & eqn : eqns) {
+            if (auto r = mk_equation(lctx, eqn, idx)) {
+                R.push_back(*r);
+                lean_assert(length(R[0].m_patterns) == length(r->m_patterns));
+            } else {
+                lean_assert(eqns.size() == 1);
+                return list<equation>();
+            }
+            idx++;
+        }
+        return to_list(R);
+    }
+
+    program mk_program(local_context const & lctx, expr const & e) {
+        lean_assert(is_equations(e));
+        buffer<expr> eqns;
+        to_equations(e, eqns);
+        unsigned arity   = get_arity(lctx, e);
+        program P;
+        expr fn_type  = binding_domain(eqns[0]);
+        std::tie(P.m_goal, P.m_var_stack) = mk_main_goal(lctx, fn_type, arity);
+        P.m_equations = mk_equations(lctx, eqns);
+        return P;
+    }
+
+    expr operator()(local_context const & lctx, expr const & eqns) {
+        lean_assert(equations_num_fns(eqns) == 1);
+        DEBUG_CODE({
+                type_context ctx = mk_type_context(lctx);
+                lean_assert(!is_recursive_eqns(ctx, eqns));
+            });
+        program P = mk_program(lctx, eqns);
 
         lean_unreachable();
     }
 };
 
-pair<expr, environment> elim_match(type_context & ctx, expr const & eqns) {
-    return elim_match_fn(ctx)(eqns);
+expr elim_match(environment & env, options const & opts, metavar_context & mctx,
+                local_context const & lctx, expr const & eqns) {
+    return elim_match_fn(env, opts, mctx)(lctx, eqns);
 }
 
 void initialize_elim_match() {
diff --git a/src/library/equations_compiler/elim_match.h b/src/library/equations_compiler/elim_match.h
index 5107a1c11c..f7796c9980 100644
--- a/src/library/equations_compiler/elim_match.h
+++ b/src/library/equations_compiler/elim_match.h
@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include "library/type_context.h"
 namespace lean {
-pair<expr, environment> elim_match(type_context & ctx, expr const & eqns);
+expr elim_match(environment & env, options const & opts, metavar_context & mctx, local_context const & lctx, expr const & eqns);
 void initialize_elim_match();
 void finalize_elim_match();
 }