json parse and serializer

Stream: lean4

[Alexandre Rademaker]

I am trying to play with Lean to read/write JSON files and analyze data encoded in JSON. Does anyone have used the JSON reader/writer facility in Lean4? I know about https://hackage.haskell.org/package/aeson, but I haven't understood the equivalent of the Aeson encode in Lean. My frustrated tentative so far is below

image.png