section doc string issue

Stream: general

[Bernd Losert]

This does not work:

/-- foo -/
section bar
end bar

but if I change the comment to /- foo -/, it stops complaing. Is this by design?

[Floris van Doorn]

Yes, doc strings /-- -/ are for declarations (and a couple of other entities). If you want a comment that appears in the doc (but not related to any specific declaration), use /-! -/

[Bernd Losert]

I see. Hmm...

[Bernd Losert]

I wanted to use section instead of adding a /- section about XYZ -/comment , but I guess I'll have to use a comment.

[Anne Baanen]

Bernd Losert said:

I wanted to use section instead of adding a /- section about XYZ -/comment , but I guess I'll have to use a comment.

Sorry for the late response, hopefully it still helps: the nicest way to spell section headers is /-! ### Section about XYZ -/. /-! -/ comments appear in the mathlib docs output, and ### turns the output line into a heading.