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

fix(library/tactic/goal): avoid unnecessary line break when possible

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-28 16:17:13 -07:00
parent ea739100b3
commit a3801e84d4
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/tactic/goal.cpp
View file

@ -36,7 +36,7 @@ format goal::pp(formatter const & fmt, substitution const & s) const {
if (first) first = false; else r += compose(comma(), line()); if (first) first = false; else r += compose(comma(), line());
expr l = *it; expr l = *it;
expr t = tmp_subst.instantiate(mlocal_type(l)); expr t = tmp_subst.instantiate(mlocal_type(l));
r += fmt(l) + space() + colon() + nest(indent, line() + fmt(t)); r += group(fmt(l) + space() + colon() + nest(indent, line() + fmt(t)));
} }
r = group(r); r = group(r);
r += line() + turnstile + space() + nest(indent, fmt(tmp_subst.instantiate(conclusion))); r += line() + turnstile + space() + nest(indent, fmt(tmp_subst.instantiate(conclusion)));