json strings with newlines

Stream: metaprogramming / tactics

[Alex J. Best]

Does anyone have any idea why the following breaks,

import data.json

#eval json.parse "hi\n"
#eval json.parse "{\"hi\":\"ho\n\"}"

or better yet how easy it would be to fix?
I believe this is valid JSON, but not accepted by lean.
@Eric Wieser @Edward Ayers perhaps?

[Eric Wieser]

Those both look like invalid json to me

[Alex J. Best]

I asked https://jsonlint.com/ and it thought it was fine. to be clear the escaping is just for lean, surely a string in json can have a line break in?

[Alex J. Best]

Ah but maybe json demands they are escaped

[Eric Wieser]

The second would be valid with \\n

[Alex J. Best]

Ok all is well then I guess!

[Trebor Huang]

Mandatory xkcd: https://xkcd.com/1638/