Skip to content

feat: do not have meta imply partial #11587

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
Merged
Kha merged 1 commit into from
Dec 12, 2025
Merged

feat: do not have meta imply partial #11587

Kha merged 1 commit into from
Dec 12, 2025
+6 −27

Conversation

@Kha
Copy link
Member

@Kha Kha commented Dec 10, 2025 •
edited
Loading

This PR adjusts the new meta keyword of the experimental module system not to imply partial for general consistency.

As the previous behavior can create confusion return types that are not known to be Nonempty and few defs should be meta in the first case, this special case does not appear to be worth the minor convenience.

@Kha Kha added the awaiting-mathlib We should not merge this until we have a successful Mathlib build label Dec 10, 2025
@Kha Kha force-pushed the push-tnmynstnmprl branch from ab26911 to 3a37d68 Compare December 10, 2025 16:35
@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 Dec 10, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Dec 10, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#11587
8341e83
@github-actions github-actions bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Dec 10, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Dec 10, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#11587
148dc61
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Dec 10, 2025
@leanprover-bot
Update lean-toolchain for testing leanprover/lean4#11587
af4d699
@leanprover-community-bot leanprover-community-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Dec 10, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Dec 10, 2025

@leanprover-bot leanprover-bot added the breaks-manual This is not necessarily a blocker for merging, but there needs to be a plan. label Dec 10, 2025
@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Dec 10, 2025 •
edited
Loading

Reference manual CI status:

@Kha Kha added the changelog-language Language features and metaprograms label Dec 10, 2025
Kha added a commit to Kha/quote4 that referenced this pull request Dec 11, 2025
@Kha
chore: adapt to leanprover/lean4#11587
9e9059d
Kha added a commit to leanprover-community/aesop that referenced this pull request Dec 11, 2025
@Kha
chore: adapt to leanprover/lean4#11587
3bcf90b
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Dec 11, 2025

@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Dec 11, 2025

@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Dec 11, 2025

@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Dec 11, 2025

@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Dec 11, 2025

@leanprover-bot leanprover-bot added builds-manual CI has verified that the Lean Language Reference builds against this PR and removed breaks-manual This is not necessarily a blocker for merging, but there needs to be a plan. labels Dec 12, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Dec 12, 2025

@leanprover-community-bot leanprover-community-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed awaiting-mathlib We should not merge this until we have a successful Mathlib build breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Dec 12, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Dec 12, 2025

@Kha Kha added this pull request to the merge queue Dec 12, 2025
Merged via the queue into leanprover:master with commit 520cdb2 Dec 12, 2025
43 of 55 checks passed
@Kha Kha deleted the push-tnmynstnmprl branch December 12, 2025 14:46
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

builds-manual CI has verified that the Lean Language Reference builds against this PR builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features and metaprograms mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@Kha @leanprover-community-bot @leanprover-bot