Style: Documenting Proofs

Stream: mathlib4

[Rudy Peterson]

Hello,

What is the preferred style for inling documentation for proofs?

Specifically, is there any style guides for this on Lean community (my apologies for missing this).

Thank you!

[Weiyi Wang]

Are you asking about -- comment vs /- comment -/in the middle of a proof? Last time I used -- comment in a long PR and it was accepted, so I guess that was fine

[Kim Morrison]

Use -- is it's only a line or two, /- if you're writing paragraphs.