Commit 2026-05-11 22:46 1be34314

feat(to_additive): support (attr := reassoc) (#38994) This PR uses registerGeneratingAttr, so that to_additive (attr := reassoc) also tags the _assoc lemma with to_additive. This interacts awkwarly with to_dual (attr := reassoc), because in that case, the reassoc attribute is responsible for handling the to_dual attribute. This is solved by adding a check so that we only insert a new translation if it doesn't already exist (e.g. because reassoc could have added it).