Zulip Chat Archive

Stream: general

Topic: congr'


Patrick Massot (May 23 2018 at 10:49):

Out of curiosity only: what is the reason for the congr_n to congr' renaming? The new name seems less descriptive to me

Mario Carneiro (May 23 2018 at 10:52):

because now it's a replacement for congr

Mario Carneiro (May 23 2018 at 10:52):

it does the effect of both congr and congr_n

Mario Carneiro (May 23 2018 at 10:52):

the integer argument is optional

Patrick Massot (May 03 2020 at 12:44):

What is the current status of congr'? Has it been moved to core and renamed congr?

Patrick Massot (Jul 03 2020 at 16:58):

Related to https://github.com/leanprover-community/lean/issues/124, @Gabriel Ebner would it be welcome to have a PR trying to replace the core congr with mathlib congr'?

Gabriel Ebner (Jul 03 2020 at 17:04):

Yes, please.

Patrick Massot (Jul 03 2020 at 17:08):

Oh, Zulip tells me I already asked about it in the very same thread on May 3rd. I guess it means I really need to do it.


Last updated: Dec 20 2023 at 11:08 UTC