expand_exists questions

Stream: general

[Rémy Degenne]

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_theory open and use [expand_exists def_name] I do not get measure_theory.def_name, but _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]

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 to_additive uses.

[Rob Lewis]

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]

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.