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

fix(library/tactic/intro_tactic): fix 'intron' tactic

Browse source
This commit is contained in:
Leonardo de Moura 2016-06-21 16:30:26 -07:00
parent 2a2d7530b2
commit 6fa6554b4d
1 changed files with 6 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/library/tactic/intro_tactic.cpp
View file

@ -53,7 +53,12 @@ optional<tactic_state> intron(unsigned n, tactic_state const & s, buffer<name> &
optional<local_decl> d = lctx.get_local_decl(new_Hs[i]);
expr type = d->get_type();
type = abstract_locals(type, i, new_Hs.data());
new_val = mk_lambda(d->get_pp_name(), type, new_val, d->get_info());
if (auto letval = d->get_value()) {
letval = abstract_locals(*letval, i, new_Hs.data());
new_val = mk_let(d->get_pp_name(), type, *letval, new_val);
} else {
new_val = mk_lambda(d->get_pp_name(), type, new_val, d->get_info());
}
}
lean_assert(!mctx.is_assigned(new_M));
mctx.assign(head(s.goals()), new_val);