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

feat(frontends/lean): use uniform delimiter

Browse source
This commit is contained in:
Leonardo de Moura 2015-07-27 18:45:33 -07:00
parent 3fb16d6287
commit 0786841c71
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -264,9 +264,9 @@ void elaborator::instantiate_info(substitution s) {
goal g(meta, meta_type);
proof_state ps(goals(g), s, m_ngen, constraints());
auto out = regular(env(), ios());
out << "LEAN_HOLE_INFORMATION\n";
out << "LEAN_INFORMATION\n";
out << ps.pp(env(), ios()) << endl;
out << "END_LEAN_HOLE_INFORMATION\n";
out << "END_LEAN_INFORMATION\n";
}
if (infom()) {
m_pre_info_data.instantiate(s);
@ -1843,13 +1843,13 @@ void elaborator::show_goal(proof_state const & ps, expr const & end, expr const
m_ctx.reset_show_goal_at();
goals const & gs = ps.get_goals();
auto out = regular(env(), ios());
out << "LEAN_GOAL_INFORMATION\n";
out << "LEAN_INFORMATION\n";
if (empty(gs)) {
out << "no goals\n";
} else {
out << head(gs) << "\n";
}
out << "END_LEAN_GOAL_INFORMATION\n";
out << "END_LEAN_INFORMATION\n";
}
bool elaborator::try_using_begin_end(substitution & subst, expr const & mvar, proof_state ps, expr const & pre_tac) {