Documentation strings

Stream: general

[Joe Hendrix]

Is there a convention in Lean for attaching documentation to specific declarations as in Haddock or Javadoc?

[Reid Barton]

Yes. use --- or /-- ... -/

[Joe Hendrix]

Does that show up in the Emacs or VSCode interfaces? I'm using the emacs interface primarily.

[Joe Hendrix]

Surprisingly, I get an error command expected when I use the /-- ... -/ syntax in front of a record field name. So it seems like there is some parsing.

[Simon Hudon]

In emacs, it should show you the doc string in the minibuffer.

Surprisingly, I get an error command expected when I use the /-- ... -/ syntax in front of a record field name.

I think they are only allowed on declarations (theorem, def, constant, etc) and not on their components.

[Joe Hendrix]

Thanks! I see it now.

[Mario Carneiro]

for other places in a definition you should just use normal comments (-- or /- -/), not doc comments