JSON libraries?

Stream: new members

[Stuart Hungerford]

Hi all — I’m interested in using Lean as a general purpose FP language. Has anyone created a library for parsing JSON? Or maybe YAML? I think there’s an example JSON parser in the Lean 4 test suite?

[Eric Wieser]

There is a docs#json library in Lean3 core

[Eric Wieser]

Although note it does not support parsing arbitrary-precision integers

[Mario Carneiro]

There is a JSON parser in lean 4 core too (docs4#Lean.Json.parse) - it's used to implement the LSP server

[Mario Carneiro]

No YAML as far as I know

[Stuart Hungerford]

Excellent!