custom docstring

Stream: general

[Yury G. Kudryashov]

Hi, I want to adjust to_additive user tag to allow something like

/-- Multiplicative docstring -/
@[to_additive add_lemma "Additive docstring"]
lemma mul_lemma : true := sorry

Do we have a parser for something like "quoted string" in Lean?

[Yury G. Kudryashov]

Another approach is to turn tactic.add_doc_string into an interactive command, but it needs a similar parser.

[Wojciech Nawrocki]

If you know the name of the additive lemma, run_cmd tactic.add_doc_string `add_lemma "Additive docstring" should work.

[Kevin Buzzard]

The issue is that we'd like to do the whole thing in one go

[Keeley Hoek]

@Yury G. Kudryashov to parse the quoted string just use the texpr parser, then eval_expr to string