Zulip Chat Archive

Stream: maths

Topic: group namespace


view this post on Zulip Chris Hughes (May 31 2019 at 16:11):

Should we not use the group namespace?

namespace group

example {α : Type*} [group α] (a b c : α) : a * b * c = a * (b * c) :=
begin
  simp [mul_assoc], -- ⊢ mul a (mul b c) = a * (b * c)
end

The trouble is it used group.mul_assoc instead of mul_assoc, so we ended up with group.mul in the goal

view this post on Zulip Mario Carneiro (May 31 2019 at 16:26):

you could use _root_.mul_assoc, or you could not be in the namespace but declare the theorem as theorem group.foo ...

view this post on Zulip Chris Hughes (May 31 2019 at 16:29):

I know, but last time this came up it took me ages to work out what was going on. Which makes things hard for people who don't know the tricks.

view this post on Zulip Mario Carneiro (May 31 2019 at 16:37):

where are we using the group namespace?

view this post on Zulip Mario Carneiro (May 31 2019 at 16:38):

Actually I think opening lots of namespaces is something I see a lot but don't really recommend

view this post on Zulip Chris Hughes (May 31 2019 at 16:46):

I was using conjugates_of_set which is in the group namespace.

view this post on Zulip Koundinya Vajjha (May 31 2019 at 17:44):

I face this issue with the integration library as well. Some results are nested within two namespaces, and I have to type out the whole thing to access them..

view this post on Zulip Mario Carneiro (May 31 2019 at 17:49):

the open command is really powerful, you should try some of the options

view this post on Zulip Johan Commelin (May 31 2019 at 18:02):

Another (currently unavailable) solution would be if we could make group.mul_assoc protected or hidden or whatever.

view this post on Zulip Johan Commelin (May 31 2019 at 18:03):

Maybe structure fields should be protected by default. Is this a reasonable feature request for 3.?.c?

view this post on Zulip Mario Carneiro (May 31 2019 at 18:06):

I don't know... that sounds like it will break peoples' things

view this post on Zulip Mario Carneiro (May 31 2019 at 18:07):

unless we give them an alternative I don't think that's reasonable


Last updated: May 11 2021 at 15:12 UTC