From b2924bba99d94aa90a3859f01e8b4308e2114625 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 1 Sep 2013 10:03:15 -0700 Subject: [PATCH] Fix typos Signed-off-by: Leonardo de Moura --- src/frontends/lean/lean_pp.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/frontends/lean/lean_pp.cpp b/src/frontends/lean/lean_pp.cpp index e9cd56713..30db7496b 100644 --- a/src/frontends/lean/lean_pp.cpp +++ b/src/frontends/lean/lean_pp.cpp @@ -861,7 +861,7 @@ class pp_fn { expr arg; unsigned s, n; is_lower(e, arg, s, n); result p_arg = pp_child(arg, depth); - format r_format = format{g_lower_fmt, colon(), format(s), colon(), format(s), nest(m_indent, compose(line(), p_arg.first))}; + format r_format = format{g_lower_fmt, colon(), format(s), colon(), format(n), nest(m_indent, compose(line(), p_arg.first))}; return mk_result(r_format, p_arg.second + 1); } @@ -869,7 +869,7 @@ class pp_fn { expr arg; unsigned s, n; is_lift(e, arg, s, n); result p_arg = pp_child(arg, depth); - format r_format = format{g_lift_fmt, colon(), format(s), colon(), format(s), nest(m_indent, compose(line(), p_arg.first))}; + format r_format = format{g_lift_fmt, colon(), format(s), colon(), format(n), nest(m_indent, compose(line(), p_arg.first))}; return mk_result(r_format, p_arg.second + 1); }