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