Commit 2022-11-22 18:22 a9b37e62

fix(Tactic/ToAdditive): deal with the auxilliary .proof_i and .eq_i declarations (#680)

• Also allow @[to_additive!]/@[to_additive?] and friends without spaces.
• I added tiny documentations because of the doc_blame linter. It would be better to use @[inherit_doc ...] on the initialization of the to_additive attribute, but I don't know the name of that. Help would be appreciated (though this can wait for a later PR).
• Add missing documentation in the rest of the file. For the other initialize attributes I copied the Lean 3 documentation that was removed in Lean 4 for some reason. I did not check if the implementation is exactly the same.