Zulip Chat Archive

Stream: general

Topic: subgroup warning


Patrick Massot (Jun 10 2020 at 19:26):

Does anyone get a message on line 250 of subgroup.lean?

Patrick Massot (Jun 10 2020 at 19:26):

I tried to rebase an old WIP on current master and I'm seeing that. I had to resolve a bunch of conflicts but I'm sure I didn't touch that file.

Yury G. Kudryashov (Jun 11 2020 at 04:37):

I'll fix it tonight.

Yury G. Kudryashov (Jun 11 2020 at 04:37):

And replace a warning with something more understandable.

Yury G. Kudryashov (Jun 11 2020 at 04:38):

It tries to say that to_additive autogenerates the same name as the one given in the argument, so "of_sub" can be safely removed.


Last updated: Aug 03 2023 at 10:10 UTC