Zulip Chat Archive

Stream: general

Topic: custom docstring

Yury G. Kudryashov (Aug 10 2019 at 06:33):

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 (Aug 10 2019 at 06:34):

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

Wojciech Nawrocki (Aug 11 2019 at 12:44):

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

Kevin Buzzard (Aug 11 2019 at 13:56):

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

Keeley Hoek (Aug 11 2019 at 23:46):

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

Last updated: Aug 03 2023 at 10:10 UTC