Commit 2024-12-10 02:18 8544aa52
View on Github →chore: fix some notation commands (#19844)
- These notations were not used in the pretty-printer. Now they are.
- Exception: The notation in
Mathlib/Algebra/Category/Grp/EpiMono.lean
still doesn't pretty-print correctly. This is still an improvement, because the previous command didn't declare the notation correctly, and it was unused in the rest of the file. - There is more to do (everything with
set_option quotPrecheck false
is suspicious).