Zulip Chat Archive
Stream: general
Topic: libary/init/algebra/group
Kenny Lau (Apr 21 2018 at 23:23):
L165:
/- αdditive "sister" structures.
alpha-dditive??
Kenny Lau (Apr 21 2018 at 23:24):
is that an easter egg
Mario Carneiro (Apr 21 2018 at 23:45):
I tried to PR that almost a year ago and of course it was rejected
Kenny Lau (Apr 21 2018 at 23:45):
lol
Kenny Lau (Apr 21 2018 at 23:45):
what was the reason
Mario Carneiro (Apr 21 2018 at 23:47):
Leo doesn't want to hear about tiny changes
Kevin Buzzard (Apr 21 2018 at 23:48):
that one must be hard to review or something
Patrick Massot (Apr 21 2018 at 23:48):
That one was provocation
Mario Carneiro (Apr 21 2018 at 23:48):
It's not an easter egg, it's a bad find-replace job when we moved from using A B C to α β γ for types
Kevin Buzzard (Apr 21 2018 at 23:48):
it's a pretty spectacular bad find-replace job!
Patrick Massot (Apr 21 2018 at 23:49):
We'll need to be much more careful when we'll to the s/α/G/g in all group theory files
Kevin Buzzard (Apr 21 2018 at 23:49):
Did they change every A to an alpha and then change 100 alpha's back to A's?
Kevin Buzzard (Apr 21 2018 at 23:50):
put it in the pile for the one time patch
Mario Carneiro (Apr 21 2018 at 23:50):
an easter egg would be replacing A with a capital alpha
Patrick Massot (Apr 21 2018 at 23:52):
variables (Α : Type) (A : Type)
Patrick Massot (Apr 21 2018 at 23:52):
Yeah!
Patrick Massot (Apr 21 2018 at 23:52):
Lean doesn't complain
Mario Carneiro (Apr 21 2018 at 23:52):
no, that's shadowing
Mario Carneiro (Apr 21 2018 at 23:52):
but universe shadowing is disallowed for some reason...
Patrick Massot (Apr 21 2018 at 23:53):
No, I the first one wasn't a capital alpha Lean would complain
Mario Carneiro (Apr 21 2018 at 23:54):
I stand corrected
Patrick Massot (Apr 21 2018 at 23:54):
Anyway, I should be sleeping
Patrick Massot (Apr 21 2018 at 23:55):
See you!
Kenny Lau (Apr 21 2018 at 23:58):
I just woke up
Last updated: Dec 20 2023 at 11:08 UTC