max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/equations_compiler/elim_match): add noequation transition

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-22 13:53:35 -07:00
parent 714817edd5
commit d8447b4c53
1 changed files with 8 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/library/equations_compiler/elim_match.cpp
View file

@ -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. */