Docstring on constructor

Stream: new members

[Wojciech Nawrocki]

How can I put a docstring on a particular constructor?

inductive commented
| a /- hello-/
| b /-- world -/
| c /- error: expected command -/

[Mario Carneiro]

can't

[Mario Carneiro]

use regular comments

[Simon Hudon]

Would it be worth adding in 3.5?

[Wojciech Nawrocki]

I would say so, but this might be a significant change. Right now Lean expects a command after a docstring. There is also a stupid workaround:

run_cmd add_doc_string ``commented.b "world"

EDIT: or maybe the parser for inductive types should not stop when seeing a doc block

[Wojciech Nawrocki]

I think as an excuse to learn the Lean sources a bit, I could give implementing this a stab.

[Wojciech Nawrocki]

This is a little more annoying than I thought, basically because in the following comment A applies to a ctr, but comment B applies to the next inductive, bar.

inductive foo: Type
/-- A -/
| mk_foo: foo
/-- B-/
inductive bar: Type

Which means the parser has to do lookahead to determine what the doc-block applies to. Is it okay to do that?
EDIT: I made a PR on community Lean, but the lookahead issue remains.