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

fix(frontends/lean/elaborator): apply substitution before compiling pre-tactics into tactics

Browse source 
closes #415
This commit is contained in:
Leonardo de Moura 2015-01-28 13:32:56 -08:00
parent 1119a8018a
commit e4b5e07498
2 changed files with 20 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1539,8 +1539,9 @@ void elaborator::try_using_begin_end(substitution & subst, expr const & mvar, pr
lean_assert(is_begin_end_annotation(pre_tac));
buffer<expr> pre_tac_seq;
extract_begin_end_tactics(get_annotation_arg(pre_tac), pre_tac_seq);
for (expr const & ptac : pre_tac_seq) {
if (auto tac = pre_tactic_to_tactic(ptac)) {
for (expr ptac : pre_tac_seq) {
expr new_ptac = subst.instantiate_all(ptac);
if (auto tac = pre_tactic_to_tactic(new_ptac)) {
try {
proof_state_seq seq = (*tac)(env(), ios(), ps);
auto r = seq.pull();
@ -1600,7 +1601,7 @@ void elaborator::solve_unassigned_mvar(substitution & subst, expr mvar, name_set
return;
}
if (auto tac = pre_tactic_to_tactic(*pre_tac)) {
if (auto tac = pre_tactic_to_tactic(subst.instantiate_all(*pre_tac))) {
bool show_failure = true;
try_using(subst, mvar, ps, *tac, show_failure);
return;

16
tests/lean/run/415.hlean Normal file
View file

@ -0,0 +1,16 @@
import algebra.group
open path_algebra
variable {A : Type}
variable [s : add_comm_group A]
include s
theorem add_minus_cancel_left1 (a b c : A) : (c + a) - (c + b) = a - b :=
begin
rotate_left 1,
apply sorry
end
theorem add_minus_cancel_left2 (a b c : A) : (c + a) - (c + b) = a - b :=
by rotate_left 1;
apply sorry