Commit 2024-12-22 16:53 2f4156e1

View on Github →

feat(to_additive): option to not translate operations on a type (#19297)

  • Also some cleanup in the ToAdditive/Frontend file (please review the first 3 commits separately), only the second commit actually changes the functionality of to_additive. The main cleanups: move doc-strings to the syntax declarations, remove the module doc which was just duplicating the to_additive-doc, and let a few internal functions depend on Environment instead of multiple other arguments.
  • In #19687 this is done for Monoid.End (in a separate PR, since that requires some library fixes).

Estimated changes

deleted def endCapitalNames
added def Test.MonoidEnd
added theorem Test.monoidEnd_lemma