to_additive and namespaces

Stream: general

[Damiano Testa]

Dear All,

playing around with to_additive, I noticed what happens below. Briefly, in the presence of namespaces, to_additive does not necessarily pick up that the auto-generated name coincides with the explicitly assigned one, even though they do.

I do not think that this is a big deal, but was puzzled by it and thought that maybe someone would be interested!

import algebra.group.defs

--  `to_additive` does *not* complain
@[to_additive add_group.add_add]
lemma group.mul_mul {G} [group G] (g : G) : true := trivial
--  the check works, regardless of whether the name is explicitly given
#check add_group.add_add

namespace group
--  `to_additive` does *not* complain
@[to_additive add_group.add_add_zero]
lemma mul_mul_one {G} [group G] (g : G) : true := trivial
--  the check works, regardless of whether the name is explicitly given
#check add_group.add_add_zero

--  `to_additive` *complains*
@[to_additive add_zero_add]
lemma mul_one_mul {G} [group G] (g : G) : true := trivial

end group