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

fix(frontends/lean/pp): do not pp let type when m_binder_types == false

Browse source
This commit is contained in:
Leonardo de Moura 2018-09-11 17:54:24 -07:00
parent d814ee612a
commit 3ba777e709
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

@ -1165,7 +1165,7 @@ auto pretty_fn::pp_let(expr e) -> result {
format sep = i < sz - 1 ? comma() : format();
format entry = format(n);
format v_fmt = pp_child(v, 0).fmt();
if (is_neutral_expr(t)) {
if (!m_binder_types || is_neutral_expr(t)) {
entry += space() + *g_assign_fmt + nest(m_indent, line() + v_fmt + sep);
} else {
format t_fmt = pp_child(t, 0).fmt();