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

chore: use new fun syntax in old pretty printer

Browse source
This commit is contained in:
Leonardo de Moura 2020-06-17 18:42:31 -07:00
parent 7ece1172a3
commit 196435c73b
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -828,9 +828,10 @@ auto pretty_fn::pp_lambda(expr const & e) -> result {
locals.push_back(p.second);
b = p.first;
}
format r = m_unicode ? *g_lambda_n_fmt : *g_lambda_fmt;
// format r = m_unicode ? *g_lambda_n_fmt : *g_lambda_fmt;
format r = *g_lambda_fmt;
r += pp_binders(locals);
r += group(compose(format(","), nest(m_indent, compose(line(), pp_child(b, 0).fmt()))));
r += group(compose(format(" =>"), nest(m_indent, compose(line(), pp_child(b, 0).fmt()))));
return result(0, r);
}