Delimiters should go on their own line in multiline docs

[Rida-Hamadani]

Check this topic on Zulip.

[grunweg]

I randomly came across this PR. My understanding is that zulip consensus is a bit different:

• for "short" doc-strings, it's fine to keep the delimiters on separate lines
• if a doc-string spans multiple paragraphs, it should certainly have delimiters on separate lines
• there were also some discussions around indentation; I'm not sure if these converged already. (I'm similarly not 100% sure if there was another aspect that I'm not remembering right now.)

Thus, a good next step could be to re-read the zulip discussions, summarise the consensus there, see if there are outstanding questions and clarify them - and then update or re-create this PR.

[Rida-Hamadani]

Thanks for commenting on this, I forgot about it!
Regarding point (3): after resolving the merge conflict, indentation was addressed in line 91.
Do you mean in (1) and (2) that you could have a multi-line "short" doc-string, cf. Kyle's message #lean4 > style guide for comments? @ 💬?
It is not clear to me whether this is the current consensus, considering that it is harder to quantify or automate.