Commit 2022-07-16 08:56 8963fcfc

feat(data/json): helper functions for json serialization (#15207) The key feature here is:

@[derive non_null_json_serializable]
structure my_type (yval : bool) :=
(x : nat)
(f : fin x)
(y : bool := tt)
(h : y = yval)

which generates the obvious serialization to json and deserialization from json of the above type. This makes communicating with other external programs a lot easier, rather than having to manually write code to disassemble json into lean structures.