diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 7701f53e35..6767bb6b36 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -195,37 +195,38 @@ lean::format pp_aux(lean::expr const & a) { return format(const_name(a)); case expr_kind::App: { - format r("("); + format r; for (unsigned i = 0; i < num_args(a); i++) { if (i > 0) r += format(" "); r += pp_aux(arg(a, i)); } - r += format(")"); - return r; + return paren(r); } case expr_kind::Lambda: - return format{format("(\u03BB ("), /* Use unicode lambda */ - format(abst_name(a)), - format(" : "), - pp_aux(abst_type(a)), - format(") "), - pp_aux(abst_body(a)), - format(")")}; + return paren(format{ + highlight(format("\u03BB "), format::format_color::PINK), /* Use unicode lambda */ + paren(format{ + format(abst_name(a)), + format(" : "), + pp_aux(abst_type(a))}), + format(" "), + pp_aux(abst_body(a))}); case expr_kind::Pi: - return format{format("(\u03A0 ("), /* Use unicode Pi */ - format(abst_name(a)), - format(" : "), - pp_aux(abst_type(a)), - format(") "), - pp_aux(abst_body(a)), - format(")")}; + return paren(format{ + highlight(format("\u03A0 "), format::format_color::ORANGE), /* Use unicode lambda */ + paren(format{ + format(abst_name(a)), + format(" : "), + pp_aux(abst_type(a))}), + format(" "), + pp_aux(abst_body(a))}); case expr_kind::Type: { std::stringstream ss; ss << ty_level(a); - return format{format("(Type "), - format(ss.str()), - format(")")}; + + return paren(format{format("Type "), + format(ss.str())}); } case expr_kind::Numeral: return format(num_value(a)); diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp index 75160743c1..af0eaedda3 100644 --- a/src/tests/kernel/expr.cpp +++ b/src/tests/kernel/expr.cpp @@ -190,6 +190,12 @@ void tst5() { expr r2 = max_sharing(r1); std::cout << "count(r1): " << count(r1) << "\n"; std::cout << "count(r2): " << count(r2) << "\n"; + std::cout << "r1 = " << std::endl; + pp(r1); + std::cout << std::endl; + std::cout << "r2 = " << std::endl; + pp(r2); + std::cout << std::endl; lean_assert(r1 == r2); } { @@ -251,6 +257,10 @@ void tst8() { r = lambda("y", p, app(lambda("x", p, var(0)), var(1))); lean_assert(!closed(r)); lean_assert(closed(lambda("z", p, r))); + + pp(lambda("y", p, app(lambda("x", p, y), var(0)))); std::cout << std::endl; + pp(pi("x", p, f(f(f(a))))); std::cout << std::endl; + } void tst9() {