-
Notifications
You must be signed in to change notification settings - Fork 883
fix: split universe levels for le_of_forall_le lemma#14133
Draft
volodeyka wants to merge 1 commit into
Draft
Conversation
@github-actions
github-actions
Bot
added
the
toolchain-available
A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
label
Jun 21, 2026
Mathlib CI status (docs):
- ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the
nightly-with-mathlibbranch. Trygit rebase 7821657e0630f8e0dd487658de0459202fd55670 --onto bc5f89f4abe82ee105ce7922a83e286fd7a67774. You can force Mathlib CI using theforce-mathlib-cilabel. (2026年06月21日 15:59:38)
leanprover-bot
commented
Jun 21, 2026
Collaborator
Reference manual CI status:
- ❗ Reference manual CI will not be attempted unless your PR branches off the
nightly-with-manualbranch. Trygit rebase 7821657e0630f8e0dd487658de0459202fd55670 --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using theforce-manual-cilabel. (2026年06月21日 15:59:39)
volodeyka
commented
Jun 21, 2026
Contributor
Author
Ah unfortunately, SymM-apply's universe bug is blocking this PR. I will merge it once it is fixed
This file contains hidden or 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
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 PR makes some
mvcgen'lemmas more universe-polymorphic. This is especially important when we work with a polymorphic monad stack.