From e765105ea5a872daa62f0a6aa6d4b0fac5f6131c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 25 Oct 2013 12:30:39 -0700 Subject: [PATCH] fix(frontends/lean/pp): let expressions Signed-off-by: Leonardo de Moura --- 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 32631e357..1dbedf9a3 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -966,10 +966,10 @@ class pp_fn { name const & n = std::get<0>(b); format beg = i == 0 ? space() : line(); format sep = i < sz - 1 ? comma() : format(); - result p_def = pp(std::get<2>(b), depth+1); + result p_def = pp_scoped_child(std::get<2>(b), depth+1); expr type = std::get<1>(b); if (type) { - result p_type = pp(type, depth+1); + result p_type = pp_scoped_child(type, depth+1); r_format += nest(3 + 1, compose(beg, group(format{format(n), space(), colon(), nest(n.size() + 1 + 1 + 1, compose(space(), p_type.first)), space(), g_assign_fmt, nest(m_indent, format{line(), p_def.first, sep})})));