Zulip Chat Archive

Stream: new members

Topic: to_additive and nested namespaces


Amelia Livingston (Dec 11 2019 at 19:55):

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 (Dec 13 2019 at 00:34):

Indeed this is not documented. Try

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

Yury G. Kudryashov (Dec 13 2019 at 00:36):

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 (Dec 13 2019 at 00:37):

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

Amelia Livingston (Dec 13 2019 at 20:28):

Thank you so much, this works great!


Last updated: Dec 20 2023 at 11:08 UTC