mathlib3
b93a64da - fix(data/json): `rbmap string α` never serializes to `null` (#15622)

Commit

3 years ago

fix(data/json): `rbmap string α` never serializes to `null` (#15622) This change means that `option (rbmap string α)` can now serialize

Author

eric-wieser

Parents