diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index d649564a18..cc66c92099 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -1202,6 +1202,7 @@ auto pretty_fn::pp_notation_child(expr const & e, unsigned lbp, unsigned rbp) -> } if (m_strings) { if (auto r = to_string(e)) return pp_string_literal(*r); + if (auto r = to_char(e)) return pp_char_literal(*r); } expr const & f = app_fn(e); if (is_implicit(f)) { @@ -1579,6 +1580,7 @@ auto pretty_fn::pp(expr const & e, bool ignore_hide) -> result { } if (m_strings) { if (auto r = to_string(e)) return pp_string_literal(*r); + if (auto r = to_char(e)) return pp_char_literal(*r); } if (auto t = is_proof(e)) { return pp_proof_type(*t);