max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(frontends/lean/pp): pp for mutual definitions

Browse source 
missing line break
This commit is contained in:
Leonardo de Moura 2017-05-18 11:46:14 -07:00
parent cf9a5128c1
commit 323060df26
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/frontends/lean/pp.cpp
View file

@ -1084,7 +1084,7 @@ auto pretty_fn::pp_equations(expr const & e) -> optional<result> {
unsigned eqnidx = 0;
for (unsigned fidx = 0; fidx < num_fns; fidx++) {
if (num_fns > 1) {
r += format("with") + space() + pp(fns[fidx]).fmt() + space() + colon() +
r += line() + format("with") + space() + pp(fns[fidx]).fmt() + space() + colon() +
space() + pp(mlocal_type(fns[fidx])).fmt();
}
if (eqnidx >= eqns.size()) return optional<result>();