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] - chore(*): update to Lean 3.14.0 #2756
Conversation
LGTM, except for the PR title. The build took only 45 minutes, is this a new record? bors d+ |
✌️ PatrickMassot can now approve this pull request. To approve and merge a pull request, simply reply with |
It seems your bet worked. |
bors merge |
Linting really did take as long as the build here! |
This is an optimistic PR, betting *nothing* will break when moving to Lean 3.14.0.
Build failed (retrying...):
|
This is an optimistic PR, betting *nothing* will break when moving to Lean 3.14.0.
Build failed:
|
bors r+ |
This is an optimistic PR, betting *nothing* will break when moving to Lean 3.14.0.
Pull request successfully merged into master. Build succeeded: |
… proof (depends on #2756) (#2758) This formalizes the proof of an old conjecture: `is_awesome Gabriel`. I also took the opportunity to remove type class struggling, which I think is related to the proof of `is_awesome Floris`. I think @jcommelin should also update this sensitivity file to use his sum notations if applicable. Co-authored-by: Johan Commelin <johan@commelin.net>
This is an optimistic PR, betting *nothing* will break when moving to Lean 3.14.0.
… proof (depends on leanprover-community#2756) (leanprover-community#2758) This formalizes the proof of an old conjecture: `is_awesome Gabriel`. I also took the opportunity to remove type class struggling, which I think is related to the proof of `is_awesome Floris`. I think @jcommelin should also update this sensitivity file to use his sum notations if applicable. Co-authored-by: Johan Commelin <johan@commelin.net>
This is an optimistic PR, betting nothing will break when moving to Lean 3.14.0.