Commit 2022-12-02 17:02 c06bd6a7

feat: to_additive can reorder arguments of generated declaration (#818)

• This allows @[to_additive] on lemmas about Pow without having to write the corresponding lemmas about SMul explicitly.
• Add syntax to_additive (reorder := ...) that will automatically reorder the arguments in the additive declaration and will reorder the arguments in all future uses of to_additive
• Deprecate @[to_additive_reorder] attribute.
  • We keep it for now, so that it can display a warning message when porting a file with the attribute
  • We allow @[to_additive (reorder := ...)] on declarations that are already additivized, so that we can give the reorder information to projections of structures.
• Maybe at some point we can add a syntax to "doubly additivize" a declaration about Pow, so that it generates both the SMul and VAdd declarations.