New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Regression after disabling `ConcreteCategory.instFunLike` as a global instance #13342

Open

dagurtomas opened this issue May 29, 2024 · 0 comments

Collaborator

dagurtomas commented May 29, 2024

#13170 disables the accidentally global instance ConcreteCategory.instFunLike. This results in some rws and simps being replaced by erw

The text was updated successfully, but these errors were encountered:

dagurtomas mentioned this issue

[Merged by Bors] - chore(Category/TopCat): cleanup #13170

Closed

mathlib-bors bot pushed a commit that referenced this issue


          chore(Category/TopCat): cleanup (#13170)

6d39f51

This PR removes an instance (`ConcreteCategory.instFunLike`) that was mistakenly made global during the port and starts the clean up. It significantly speeds up CI since simp is more efficient.

Unfortunately, some `simp`'s and `rw`'s needed to be changed to `erw` as a result.

Zulip discussion: [#mathlib4 > ConcreteCategory.instFunLike became a global instance](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/ConcreteCategory.2EinstFunLike.20became.20a.20.20global.20instance)

Issue: #13342 



Co-authored-by: Matthew Ballard <[email protected]>
Co-authored-by: dagurtomas <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: erdOne <[email protected]>
Co-authored-by: Dagur Tómas Ásgeirsson <[email protected]>

callesonne pushed a commit that referenced this issue


          chore(Category/TopCat): cleanup (#13170)

b59de54

This PR removes an instance (`ConcreteCategory.instFunLike`) that was mistakenly made global during the port and starts the clean up. It significantly speeds up CI since simp is more efficient.

Unfortunately, some `simp`'s and `rw`'s needed to be changed to `erw` as a result.

Zulip discussion: [#mathlib4 > ConcreteCategory.instFunLike became a global instance](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/ConcreteCategory.2EinstFunLike.20became.20a.20.20global.20instance)

Issue: #13342 



Co-authored-by: Matthew Ballard <[email protected]>
Co-authored-by: dagurtomas <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: erdOne <[email protected]>
Co-authored-by: Dagur Tómas Ásgeirsson <[email protected]>

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment