mathlib
92f31fbc - refactor(tactic/polyrith): use the autogenerated json parser (#15429)

Commit

3 years ago

refactor(tactic/polyrith): use the autogenerated json parser (#15429) This acts as a nice demonstration of how to use `@[derive non_null_json_serializable]`

Author

eric-wieser

Parents

0b673ed4

mathlib 92f31fbc - refactor(tactic/polyrith): use the autogenerated json parser (#15429)

mathlib
92f31fbc - refactor(tactic/polyrith): use the autogenerated json parser (#15429)