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

feat(frontends/lean/elaborator): display the whole proof state in option "--goal"

Browse source 
see issue #755
This commit is contained in:
Leonardo de Moura 2015-07-31 08:55:14 -07:00
parent a53ac25ca8
commit 8f5a760b89
1 changed files with 1 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1849,17 +1849,10 @@ void elaborator::show_goal(proof_state const & ps, expr const & start, expr cons
if (curr_pos->first < line || (curr_pos->first == line && curr_pos->second < col))
return;
m_ctx.reset_show_goal_at();
goals const & gs = ps.get_goals();
auto out = regular(env(), ios());
print_lean_info_header(out.get_stream());
out << "position " << curr_pos->first << ":" << curr_pos->second << "\n";
if (empty(gs)) {
out << "no goals\n";
} else {
goal g = head(gs);
g = g.instantiate(ps.get_subst());
out << g << "\n";
}
out << ps.pp(env(), ios()) << "\n";
print_lean_info_footer(out.get_stream());
}