Non-docstring comments before declarations

Stream: mathlib4

[Yury G. Kudryashov]

I've recently noticed some comments that were clearly meant to be docstrings, but accidentally used /- instead of /--. Should we have a syntax linter that warns against it?

[Johan Commelin]

Good idea: I've created https://github.com/mathlib-initiative/TaskList/issues/41