Zulip Chat Archive

Stream: maths

Topic: modules


view this post on Zulip Johan Commelin (Jan 30 2019 at 08:05):

Can someone (@Mario Carneiro, @Kenny Lau) explain why exactly one needs [add_comm_group M] before being able to speak about [module M]?

view this post on Zulip Mario Carneiro (Jan 30 2019 at 08:06):

because it's not [module M] anymore, it's [module R M]

view this post on Zulip Kenny Lau (Jan 30 2019 at 08:06):

Because the parent coercion module R M => add_comm_group M was causing much of the module typeclass issues

Mario Carneiro, 13:48 (UTC), 2018 Nov 05

view this post on Zulip Mario Carneiro (Jan 30 2019 at 08:07):

after Kenny's refactoring, we definitely need add_comm_group separate

view this post on Zulip Johan Commelin (Jan 30 2019 at 08:07):

Ok

view this post on Zulip Mario Carneiro (Jan 30 2019 at 08:07):

in short, it's the part of the module structure that doesn't depend on R

view this post on Zulip Johan Commelin (Jan 30 2019 at 08:07):

Sure


Last updated: May 11 2021 at 16:22 UTC