Standardizing to_additive docstrings

Stream: general

[Eric Wieser]

We seem to have two different styles for additivizing docstrings:

/-- this is `mul_foo` -/
@[to_additive /-" this is `add_foo` "-/]
def mul_foo : sorry = sorry

and

/-- this is `mul_foo` -/
@[to_additive "this is `add_foo`"]
def mul_foo : sorry = sorry

Is there any preference between these styles?

The former has the advantage of highlighting like a comment with markdown in vs-code (mainly useful for backticks) and no special escaping needed for ", but the disadvantage of being hard to type and easy to mistype as /- lost "-/ which makes it an actual comment that ends up ignored.

[Eric Wieser]

/poll Which you do prefer?

[Alex J. Best]

Is the voting here about what people prefer personally, or if we think there should be standardization, this is something I don't think we need to worry about standardizing, and indeed have no preference between the two myself. So there is no option for me to select in your poll, I can add a new one of course

[Eric Wieser]

(ignoring the question of "is it a waste of time to change this everywhere", to which the answer is certainly "yes" - we could still advocate for one or the other in new code)

[Eric Wieser]

A vote for both is probably a ok indication of "don't care". Or add a new option.