cons overload

Stream: general

[Kenny Lau]

kinda annoyed by the fact that list.cons and multiset.cons both use ::

[Kevin Buzzard]

Yes, that's the other instance of overloading other than ^

[Kevin Buzzard]

Mario has commented on this in the past. It's a great example of something which Mario would love to change but which Leo is not interested in changing.

[Kenny Lau]

I see

[Kevin Buzzard]

In the past the philosophy was always "wait".

[Kevin Buzzard]

Now we have Lean 3.4 we can again raise the possibility of a fork plus a one-time patch, to give Lean 3.400001 "modded by Mario"

[Kevin Buzzard]

Leo again made it clear that he would have no objection to a fork.

[Kevin Buzzard]

My instinct is to wait a while and to see how many commits to Lean 3.4 actually do occur in the next month or so

[Kevin Buzzard]

If things really are going to slow down then this is really exciting

[Kevin Buzzard]

because it means that Mario will not have to take time out about once a week and spend time (and possibly a highly non-trivial amount of time) fixing up mathlib because of changes in core.

[Kevin Buzzard]

You saw yourself how frustrated I got when the changes to ^ broke our stacks project code and stopped me working on the project for several days because I was not capable of fixing the code that you and Chris had written and you two had other things on your mind (completely understandably).

[Kevin Buzzard]

Why not open an issue in mathlib?

[Kevin Buzzard]

If Lean 4 is not going to be compatible with Lean 3 then this is an argument for not fussing too much about simple changes such as this.