Topic: expand_exists questions
Rémy Degenne (Jul 27 2022 at 17:36):
I am testing the new
expand_exists attribute, which looks like a very useful tool, and I have two remarks/questions:
- The names given to the new lemmas are interpreted as being names in the
_root_namespace. For example, if I have the namespace
measure_theoryopen and use
[expand_exists def_name]I do not get
_root_.def_name. I expected the opposite behaviour. Is it an intentional design decision?
- The attribute creates a def and lemmas, but the def does not have a docstring and the linter complains. Is there a way to give a dosctring when using the attribute?
Related to my second question: is it possible to give a dosctring to a definition after its declaration? I want to make the linter happy :)
Rob Lewis (Jul 27 2022 at 17:47):
Re: namespacing, I think this is fixable -- the behavior would be to put the new declarations in the same namespace as the original one. It would mimic whatever logic
Rob Lewis (Jul 27 2022 at 17:48):
Re: doc strings, are you imaginging the same syntax as
to_additive to include a doc string in the attribute? I've always kind of hated that syntax, but again, it's doable. In the meantime you can use command#add_decl_doc to add a doc string after its declaration.
Rémy Degenne (Jul 27 2022 at 17:50):
For the docstring, I don't really have a preferred way of doing it, but I did not know how to add it (I never had to use add_decl_doc). A simple note in the docstring of expand_exists reminding the user that add_decl_doc exists would be fine for me.
Last updated: Aug 03 2023 at 10:10 UTC