Commit 2021-07-05 15:47 38a6f265

feat(algebra/to_additive): map pow to smul (#7888)

• Allows @[to_additive] to reorder consecutive arguments of specified identifiers.
• This can be specified with the attribute @[to_additive_reorder n m ...] to swap arguments n and n+1, arguments m and m+1 etc. (start counting from 1).
• The only two attributes currently in use are:

attribute [to_additive_reorder 1] has_pow
attribute [to_additive_reorder 1 4] has_pow.pow

• It will eta-expand all expressions that have as head a declaration with attribute to_additive_reorder until they have the required number of arguments. This is required to correctly deal with partially applied terms.
• Hack: if the first two arguments are reordered, then the first two universe variables are also reordered (this happens to be the correct behavior for has_pow and has_pow.pow). It might be cleaner to have a separate attribute for that, but that given the low amount of times that I expect that we use to_additive_reorder, this seems unnecessary.
• This PR also allows the user to write @[to_additive?] to trace the generated declaration.