[Merged by Bors] - feat: adaptations for leanprover/lean4#2964 #9176
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
kim-em
force-pushed
the
bump_bump_2964
branch
from
9f43267 to
d72b6e3
Compare
kim-em
commented
Dec 21, 2023
eric-wieser
reviewed
Dec 21, 2023
eric-wieser
reviewed
Dec 21, 2023
| @@ -52,7 +52,7 @@ theorem join_filter_isEmpty_eq_false [DecidablePred fun l : List α => l.isEmpty | |||
| | [] :: L => by | |||
| simp [join_filter_isEmpty_eq_false (L := L), isEmpty_iff_eq_nil] | |||
| | (a :: l) :: L => by | |||
| simp [join_filter_isEmpty_eq_false (L := L), isEmpty_cons] | |||
| simp [join_filter_isEmpty_eq_false (L := L)] | |||
There was a problem hiding this comment.
Is this some merge weirdness, or genuinely intended as part of this patch?
There was a problem hiding this comment.
I'm not sure. This is what is currently on nightly-testing: it doesn't seem to be on @Vtec234's lean-pr-testing-2964 branch...
Given it's a good change I'm inclined to just sneak it in here?
|
✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors merge |
|
Already running a review |
|
Oops. |
|
bors merge |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Dec 21, 2023
This is a PR to `bump/v4.5.0`, containing the adaptations required for @Vtec234's leanprover/lean4#2964. This will bring `bump/v4.5.0` up to `nightly-2023-12-21`, which will tomorrow become `v4.5.0-rc1`. Thus once this PR is delegated and merged, Mathlib should be ready to move to the next release. Co-authored-by: Scott Morrison <[email protected]>
|
Pull request successfully merged into bump/v4.5.0. Build succeeded: |
mathlib-bors
bot
changed the title
mathlib-bors bot
pushed a commit
that referenced
this pull request
Dec 22, 2023
…h. (#9188) This PR: * bumps to lean-toolchain to `v4.5.0-rc1` * bumps the Std and Aesop dependencies to their versions using `v4.5.0-rc1` * merge the already reviewed changes from the `bump/v4.5.0` branch * adaptations for leanprover/lean4#2923 in #9011 * adaptations for leanprover/lean4#2973 in #9161 * adaptations for leanprover/lean4#2964 in #9176 Co-authored-by: Scott Morrison <[email protected]> Co-authored-by: Eric Wieser <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This is a PR to
bump/v4.5.0, containing the adaptations required for @Vtec234's leanprover/lean4#2964.These adaptations are using a pre-release version of
ProofWidgets4(v0.0.24-pre2). Afterv4.5.0-rc1becomes available, a new version ofProofWidgets4with a more strongly-typed component API will be released, and a PR will be proposed to adapt Mathlib to it.This will bring
bump/v4.5.0up tonightly-2023-12-21, which will tomorrow becomev4.5.0-rc1. Thus once this PR is delegated and merged, Mathlib should be ready to move to the next release.