diff --git a/src/library/print.cpp b/src/library/print.cpp index 32af9bd4c2..ed287028e1 100644 --- a/src/library/print.cpp +++ b/src/library/print.cpp @@ -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; } }