From 2b3af47fcf6bdc24d1f5f0fe4fd947f0603a74c4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 13 Oct 2015 17:26:27 -0700 Subject: [PATCH] feat(frontends/lean/pp): pretty print "num numerals" too This is an useful for "eval" demos --- src/frontends/lean/pp.cpp | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 3872aec59..507f84dbb 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -477,8 +477,10 @@ auto pretty_fn::pp_child(expr const & e, unsigned bp, bool ignore_hide) -> resul if (is_app(e)) { if (auto r = pp_local_ref(e)) return add_paren_if_needed(*r, bp); - if (m_numerals) + if (m_numerals) { if (auto n = to_num(e)) return pp_num(*n); + if (auto n = to_num_core(e)) return pp_num(*n); + } expr const & f = app_fn(e); if (auto it = is_abbreviated(f)) { return pp_abbreviation(e, *it, true, bp, ignore_hide); @@ -972,8 +974,10 @@ auto pretty_fn::pp_notation_child(expr const & e, unsigned lbp, unsigned rbp) -> if (auto it = is_abbreviated(e)) return pp_abbreviation(e, *it, false, rbp); if (is_app(e)) { - if (m_numerals) + if (m_numerals) { if (auto n = to_num(e)) return pp_num(*n); + if (auto n = to_num_core(e)) return pp_num(*n); + } expr const & f = app_fn(e); if (auto it = is_abbreviated(f)) { return pp_abbreviation(e, *it, true, rbp); @@ -1225,8 +1229,10 @@ auto pretty_fn::pp(expr const & e, bool ignore_hide) -> result { flet let_d(m_depth, m_depth+1); m_num_steps++; - if (m_numerals) + if (m_numerals) { if (auto n = to_num(e)) return pp_num(*n); + if (auto n = to_num_core(e)) return pp_num(*n); + } if (auto n = is_abbreviated(e)) return pp_abbreviation(e, *n, false); if (auto r = pp_notation(e))