Zulip Chat Archive

Stream: general

Topic: custom docstring


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Aug 11 2019 at 13:56):

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

view this post on Zulip 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: May 18 2021 at 16:25 UTC