michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

chore(library/blast): cleanup

Browse source
This commit is contained in:
Leonardo de Moura 2016-03-01 17:42:57 -08:00
parent 87252bbffe
commit 6f766dd33e
2 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/blast/backward/backward_lemmas.cpp
View file

@ -60,9 +60,9 @@ typedef scoped_ext<backward_config> backward_ext;
static optional<head_index> get_backward_target(tmp_type_context & ctx, expr type) {
while (is_pi(type)) {
expr local = ctx.mk_tmp_local(binding_domain(type));
type = ctx.try_to_pi(instantiate(binding_body(type), local));
type = ctx.whnf(instantiate(binding_body(type), local));
}
expr fn = get_app_fn(ctx.whnf(type));
expr fn = get_app_fn(type);
if (is_constant(fn) || is_local(fn))
return optional<head_index>(fn);
else

4
src/library/blast/grinder/intro_elim_lemmas.cpp
View file

@ -80,9 +80,9 @@ optional<name> get_intro_target(tmp_type_context & ctx, name const & c) {
expr type = ctx.try_to_pi(instantiate_type_univ_params(d, to_list(us)));
while (is_pi(type)) {
expr local = ctx.mk_tmp_local(binding_domain(type));
type = ctx.try_to_pi(instantiate(binding_body(type), local));
type = ctx.whnf(instantiate(binding_body(type), local));
}
expr const fn = get_app_fn(ctx.whnf(type));
expr const fn = get_app_fn(type);
if (is_constant(fn))
return optional<name>(const_name(fn));
else