Zulip Chat Archive

Stream: maths

Topic: modules

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]?

Mario Carneiro (Jan 30 2019 at 08:06):

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

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

Mario Carneiro (Jan 30 2019 at 08:07):

after Kenny's refactoring, we definitely need add_comm_group separate

Johan Commelin (Jan 30 2019 at 08:07):

Ok

Mario Carneiro (Jan 30 2019 at 08:07):

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

Johan Commelin (Jan 30 2019 at 08:07):

Sure

Last updated: Dec 20 2023 at 11:08 UTC