Docstring style?

Stream: mathlib4

[Thomas Murrills]

I could have sworn I'd seen something somewhere specifying the style convention for docstrings—things like don't restate the type, use present tense, etc. I can't seem to find that anymore. Does anyone know if this exists somewhere?

[Scott Morrison]

I suspect the best you'll find is https://leanprover-community.github.io/contribute/style.html

[Mario Carneiro]

there is a lean 4 core issue by Patrick Massot about the style guide

[Mario Carneiro]

lean4#1461