From 196435c73b56360da551e7b0dd28fd497d4b40f1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 17 Jun 2020 18:42:31 -0700 Subject: [PATCH] chore: use new `fun` syntax in old pretty printer --- src/frontends/lean/pp.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index f39f176013..bfc2042c2b 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -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); }