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.

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