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: May 18 2021 at 16:25 UTC