doc comments

Stream: new members

[John Hui]

Is there any documentation on doc comments? I see they're defined in the lexical structure of the refman, but it doesn't seem to say anything about the syntax within them. And what's the difference between /-- and /-!?

[Bhavik Mehta]

There's https://leanprover-community.github.io/contribute/doc.html

[John Hui]

ah thanks, didn't realize this existed!

[Bryan Gin-ge Chen]

In short, /-- and -/ surround a docstring that's assigned to a particular declaration and /-! and -/ surround a module docstring that just lives on its own in the middle of a file.

Note that the syntax for comments has changed from what's written in the reference manual. In Lean 3.6.0c and later, nesting of block / doc / module comments is allowed, e.g. /-! /- /- -/ -/ -/ is a valid module docstring in 3.6.0c but not in the officially released 3.4.2 (the module docstring terminates at the first -/).