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

feat(frontends/lean/elaborator): change behavior of "show goal" for incomplete "by tactic"

Browse source 
If "by tactic" did not completely solved the goal, then we show the
final state when the user presses "C-c C-g"
This commit is contained in:
Leonardo de Moura 2015-07-29 17:34:42 -07:00
parent b3707ab54a
commit 384ccf2b6c
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1784,27 +1784,30 @@ bool elaborator::try_using(substitution & subst, expr const & mvar, proof_state
lean_assert(length(ps.get_goals()) == 1);
// make sure ps is a really a proof state for mvar.
lean_assert(mlocal_name(get_app_fn(head(ps.get_goals()).get_meta())) == mlocal_name(mvar));
show_goal(ps, pre_tac, pre_tac, pre_tac);
try {
proof_state_seq seq = tac(env(), ios(), ps);
auto r = seq.pull();
if (!r) {
show_goal(ps, pre_tac, pre_tac, pre_tac);
// tactic failed to produce any result
if (show_failure)
display_unsolved_proof_state(mvar, ps, "tactic failed");
return false;
} else if (!empty(r->first.get_goals())) {
// tactic contains unsolved subgoals
show_goal(r->first, pre_tac, pre_tac, pre_tac);
if (show_failure)
display_unsolved_subgoals(mvar, r->first);
return false;
} else {
show_goal(ps, pre_tac, pre_tac, pre_tac);
subst = r->first.get_subst();
expr v = subst.instantiate(mvar);
subst.assign(mlocal_name(mvar), v);
return true;
}
} catch (tactic_exception & ex) {
show_goal(ps, pre_tac, pre_tac, pre_tac);
if (show_failure)
display_tactic_exception(ex, ps, pre_tac);
return false;