to_additive and nested namespaces

Stream: new members

[Amelia Livingston]

Hallo - sorry I can't work this out from the documentation in to_additive.lean, but how do I get localization.monoid to transport to add_localization.add_monoid instead?

import algebra.group.to_additive

variables (α : Type*)

@[to_additive add_localization] def localization := α

namespace localization.monoid

@[to_additive] lemma foo : true := trivial

end localization.monoid

#check add_localization.monoid.foo -- add_localization.monoid.foo : true

I don't really want to write @[to_additive add_localization.add_monoid.foo] at the beginning of everything, and attribute [to_additive add_localization.add_monoid] localization.monoid doesn't make sense because localization.monoid is an unknown identifier, and those are my only ideas :( Thank you in advance.

[Yury G. Kudryashov]

Indeed this is not documented. Try

run_cmd to_additive.map_namespace `localization.monoid `add_localization.add_monoid

[Yury G. Kudryashov]

Lean doesn't allow us to have attributes on namespaces, so to_additive.map_namespace creates an auxiliary def named src._to_additive.

[Yury G. Kudryashov]

I should probably review the to_additive documentation, and add it to tactic.md.

[Amelia Livingston]

Thank you so much, this works great!