Zulip Chat Archive

Stream: new members

Topic: doc comments

view this post on Zulip John Hui (May 19 2020 at 15:58):

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 /-!?

view this post on Zulip Bhavik Mehta (May 19 2020 at 15:59):

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

view this post on Zulip John Hui (May 19 2020 at 15:59):

ah thanks, didn't realize this existed!

view this post on Zulip Bryan Gin-ge Chen (May 19 2020 at 16:07):

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 -/).

Last updated: May 16 2021 at 21:11 UTC