Zulip Chat Archive

Stream: lean4

Topic: From/ToJson for user code


view this post on Zulip Calvin Lee (Feb 19 2021 at 23:16):

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.

view this post on Zulip Marc Huisinga (Feb 19 2021 at 23:22):

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))

view this post on Zulip Calvin Lee (Feb 20 2021 at 00:02):

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)"

view this post on Zulip Marc Huisinga (Feb 20 2021 at 00:05):

There's one for arrays, but not lists


Last updated: May 18 2021 at 22:15 UTC