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).

Estimated changes