mathlib3

8963fcfc - feat(data/json): helper functions for json serialization (#15207)

feat(data/json): helper functions for json serialization (#15207) The key feature here is: ```lean @[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.