Commit 2023-01-09 17:24 56bf4cd6

feat: improve the way to_additive deals with attributes (#1314)

• The new syntax for any attributes that need to be copied by to_additive is @[to_additive (attrs := simp, ext, simps)]
• Adds the auxiliary declarations generated by the simp and simps attributes to the to_additive-dictionary.
• Future issue: Does not yet translate auxiliary declarations for other attributes (including custom simp-attributes). In particular it's possible that norm_cast might generate some auxiliary declarations.
• Fixes #950
• Fixes #953
• Fixes #1149
• This moves the interaction between to_additive and simps from the Simps file to the toAdditive file for uniformity.
• Make the same changes to @[reassoc]