From/ToJson for user code

Stream: lean4

[Calvin Lee]

Hi! Can programmers use/derive the FromJson and ToJson classes? I see this used throughout the Lean compiler itself, but I have tried importing Lean.Data.Json and cannot seem to derive these classes.

[Marc Huisinga]

Are you using the right namespace?

import Lean.Data.Json

structure Foo where
  x : String
  y : Nat
  deriving Lean.FromJson, Lean.ToJson

instance : ToString Foo where
  toString f := s!"{f.x} {f.y}"

#eval Lean.toJson {x := "foo", y := 1 : Foo} -- {"y": 1, "x": "foo"}
#eval (Lean.fromJson? <| Lean.toJson {x := "foo", y := 1 : Foo} : Option Foo) -- (some (foo 1))

[Calvin Lee]

Oh that works! I was thinking it was in the Json namespace for some reason.
Is there some instance of ToJson and FromJson for lists? I'm getting "failed to synthesize instance FromJson (List Nat)"

[Marc Huisinga]

There's one for arrays, but not lists