Commit 2023-02-17 17:10 37ae5972

feat: to_additive raises linter errors; nested to_additive (#1819)

• Turn info messages of to_additive into linter errors
• Allow @[to_additive (attr := to_additive)] to additivize the generated lemma. This is useful for Pow -> SMul -> VAdd lemmas. We can write e.g. @[to_additive (attr := to_additive, simp)] to add the simp attribute to all 3 generated lemmas, and we can provide other options to each to_additive call separately (specifying a name / reorder).
• The previous point was needed to cleanly get rid of some linter warnings. It also required some additional changes (addToAdditiveAttr now returns a value, turn a few (meta) definitions into mutual partial def, reorder some definitions, generalize additivizeLemmas to lists of more than 2 elements) that should have no visible effects for the user.