From d8447b4c53d03578fcc8b852fa27ad42dec9aef2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 22 Aug 2016 13:53:35 -0700 Subject: [PATCH] feat(library/equations_compiler/elim_match): add noequation transition --- src/library/equations_compiler/elim_match.cpp | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/library/equations_compiler/elim_match.cpp b/src/library/equations_compiler/elim_match.cpp index 11c5c6293c..b8795113de 100644 --- a/src/library/equations_compiler/elim_match.cpp +++ b/src/library/equations_compiler/elim_match.cpp @@ -412,7 +412,14 @@ struct elim_match_fn { result compile_no_equation(program const & P) { trace_match(tout() << "no equation transition\n";); - lean_unreachable(); + type_context ctx = mk_type_context(P); + expr type = ctx.relaxed_whnf(ctx.infer(P.m_goal)); + if (!is_pi(type)) throw_ill_formed_eqns(); + expr arg_type = whnf_inductive(ctx, binding_domain(type)); + if (is_inductive_app(arg_type)) + return compile_constructor(P); + else + return compile_variable(P); } /** Return the first of pattern of the equation with the given index. */