From df1bb458f9d37da87fc4f77ce039b0ad17ef68c6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 26 Jul 2016 15:44:03 -0700 Subject: [PATCH] fix(frontends/lean/pp): use group for lambda/pi --- src/frontends/lean/pp.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index e6013a294d..8a7a8d1b98 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -791,7 +791,7 @@ auto pretty_fn::pp_lambda(expr const & e) -> result { } format r = m_unicode ? *g_lambda_n_fmt : *g_lambda_fmt; r += pp_binders(locals); - r += compose(comma(), nest(m_indent, compose(line(), pp_child(b, 0).fmt()))); + r += group(compose(comma(), nest(m_indent, compose(line(), pp_child(b, 0).fmt())))); return result(0, r); } @@ -822,7 +822,7 @@ auto pretty_fn::pp_pi(expr const & e) -> result { else r = m_unicode ? *g_pi_n_fmt : *g_pi_fmt; r += pp_binders(locals); - r += compose(comma(), nest(m_indent, compose(line(), pp_child(b, 0).fmt()))); + r += group(compose(comma(), nest(m_indent, compose(line(), pp_child(b, 0).fmt())))); return result(0, r); } }