Zulip Chat Archive

Stream: mathlib4

Topic: mathlib#17733


Scott Morrison (Nov 27 2022 at 20:22):

This PR is the attempt to revert #17048, as discussed elsewhere.

In topology/instances/add_circle we have a broken proof (this was added since #17048, so it uses the new technology).

Scott Morrison (Nov 27 2022 at 20:22):

If someone (@Oliver Nash, or anyone) wants to fix that it would be great.

Jireh Loreaux (Nov 27 2022 at 22:18):

I've tried to fix it, but I had to do it blind because I have a limited internet connection (so I can't download oleans). We'll see what CI says.

Scott Morrison (Nov 28 2022 at 02:18):

I think we're about to have a green tick here, so if someone could delegate this one that would be great.

Yury G. Kudryashov (Nov 28 2022 at 03:26):

IMHO, a better long-term solution is to tell simp about coe (i.e., treat all functions marked with coe as coe). I don't know how hard it is.

Yury G. Kudryashov (Nov 28 2022 at 03:27):

But this revert looks like a good mid-term solution.

Oliver Nash (Nov 28 2022 at 09:04):

Thank you to @Jireh Loreaux for making the required fix for add_circle! (I was just about to take this up.) It is sad to see Anne's work reverted but I agree that this is the right call given the demands of the port.

Oliver Nash (Nov 28 2022 at 09:05):

Incidentally I do plan to join in the porting effort but probably not till January.


Last updated: Dec 20 2023 at 11:08 UTC