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

chore(frontends/lean/elaborator): remove unnecessary procedure

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-10 21:14:58 -07:00
parent 318c94bfce
commit 4d06f71e72
1 changed files with 1 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/frontends/lean/elaborator.cpp
View file

@ -1251,16 +1251,6 @@ static expr update_equations_fn_type(expr const & eqns, expr const & new_fn_type
return update_equations(eqns, eqs);
}
static expr unpack_equations_result(expr const & e, expr const & ref) {
if (is_equations_result(e)) {
return get_equations_result(e, 0);
} else if (is_let(e)) {
return update_let(e, let_type(e), let_value(e), unpack_equations_result(let_body(e), ref));
} else {
throw elaborator_exception(ref, "unexpected equation compiler result");
}
}
expr elaborator::visit_convoy(expr const & e, optional<expr> const & expected_type) {
lean_assert(is_app(e));
lean_assert(is_equations(get_app_fn(e)));
@ -1324,7 +1314,7 @@ expr elaborator::visit_convoy(expr const & e, optional<expr> const & expected_ty
}
trace_elab(tout() << "match/convoy function type: " << new_fn_type << "\n";);
expr new_eqns = visit_equations(update_equations_fn_type(eqns, new_fn_type));
expr fn = unpack_equations_result(new_eqns, ref);
expr fn = get_equations_result(new_eqns, 0);
return mk_app(fn, new_args);
}