max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(frontends/lean/pp): char literals

Browse source
This commit is contained in:
Leonardo de Moura 2016-11-23 11:58:11 -08:00
parent 01bc4dfcd2
commit ffe9b3c5d6
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/pp.cpp
View file

@ -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);