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.
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
[Merged by Bors] - feat: port Data.Set.Sups #2991
Conversation
Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
Can you check what is going on here, @YaelDillies? In mathlib at commit e96bdfbd, I get a similar problem, that I see in mathlib4:
Does this need be fixed in mathlib first? |
It's because there needs to be a forward port of the dependencies first. I am writing it later today. |
This PR/issue depends on:
|
This should fix the simpNF lints, but I'm unsure if they were justified. Please take a close look and possibly revert the last two commits and fix the simpNF lint complaints differntly. |
@Parcly-Taxel, please be sure something is ready for review before marking it as such. Here there were still some plain mathport output in the file along with linters to appease. |
bors r+ |
Co-authored-by: Moritz Firsching <firsching@google.com> Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Pull request successfully merged into master. Build succeeded: |
- [x] depends on: leanprover-community/mathlib#18172 - [x] depends on: #2991 Co-authored-by: Moritz Firsching <firsching@google.com> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
- [x] depends on: leanprover-community/mathlib#18172 - [x] depends on: #2991 Co-authored-by: Moritz Firsching <firsching@google.com> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
- [x] depends on: leanprover-community/mathlib#18172 - [x] depends on: #2991 Co-authored-by: Moritz Firsching <firsching@google.com> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Set.image2_image2_image2_comm
#2992