JSON🔗

Json is one of the most widely used data formats for representing structured data. Lean 4 provides a robust module for working with Json. You can find it under import Lean.Data.Json. This chapter covers how to create, manipulate, and persist Json data in Lean.

Recipes:

1. Creating JSON Objects
2. Accessing and Modifying JSON
3. Reading & Writing JSON Files
4. Miscellaneous JSON