Zulip Chat Archive
Stream: mathlib4
Topic: Order.OmegaCompletePartialOrder mathlib4#1168
Johan Commelin (Jan 17 2023 at 10:41):
This PR has lots of simps problems.
Johan Commelin (Jan 17 2023 at 10:41):
Atm they've been commented away. But I'm not sure if we should merge like that.
Chris Hughes (Jan 17 2023 at 12:56):
To be honest, all the coeFn stuff should be replaced with FunLike
Yaël Dillies (Jan 17 2023 at 14:13):
I can make the change in mathlib if you want
Chris Hughes (Jan 17 2023 at 18:02):
That would be a good change, but I've made the same change in other files without bothering to backport
Kevin Buzzard (Jan 17 2023 at 18:35):
I think that when fiddling with coercions you can get away with not backporting because "coercions have changed".
Yaël Dillies (Jan 17 2023 at 19:04):
Well, FunLike is in fact a little island of stability amidst the porting storm.
Last updated: Dec 20 2023 at 11:08 UTC