Stream: new members
Topic: doc comments
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
Bhavik Mehta (May 19 2020 at 15:59):
John Hui (May 19 2020 at 15:59):
ah thanks, didn't realize this existed!
Bryan Gin-ge Chen (May 19 2020 at 16:07):
-/ surround a docstring that's assigned to a particular declaration 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