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

fix: print for string literal

Browse source
This commit is contained in:
Leonardo de Moura 2019-12-16 07:34:40 -08:00
parent a172998954
commit 7d736e63b1
1 changed files with 5 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/library/print.cpp
View file

@ -280,8 +280,11 @@ struct print_expr_fn {
case expr_kind::Lit:
switch (lit_value(a).kind()) {
case literal_kind::Nat: out() << lit_value(a).get_nat().to_mpz(); break;
case literal_kind::String: out() << escaped(lit_value(a).get_string().data()); break; // HACK Lean string as C string
}
case literal_kind::String: {
std::string val(lit_value(a).get_string().data() + 1);
val.pop_back();
out() << "\"" << escaped(val.c_str()) << "\""; break; // HACK Lean string as C string
}}
break;
}
}