Skip to content

feat: make noConfusion even more heterogeneous #11562

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
Draft
nomeata wants to merge 7 commits into
base: master
Choose a base branch
from
Draft

feat: make noConfusion even more heterogeneous #11562

nomeata wants to merge 7 commits into from

Conversation

@nomeata
Copy link
Collaborator

@nomeata nomeata commented Dec 9, 2025

This PR makes the noConfusion principles even more heterogeneous, by allowing not just indices but also parameters to be differ.

This is a breaking change for manual use of noConfusion for types with parameters. Pass suitable rfl arguments, and use eq_of_heq on the resulting equalities as needed.

This fixes #11560.

@nomeata nomeata added the changelog-language Language features and metaprograms label Dec 9, 2025
@nomeata nomeata force-pushed the joachim/issue11560 branch from 6e08492 to e1320d7 Compare December 9, 2025 13:55
@github-actions github-actions bot added changes-stage0 Contains stage0 changes, merge manually using rebase toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN labels Dec 9, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Dec 9, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#11562
db1e6f9
@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 9, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Dec 9, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#11562
cc425d8
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Dec 9, 2025
@leanprover-bot
Update lean-toolchain for testing leanprover/lean4#11562
189c122
@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 9, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Dec 9, 2025

Mathlib CI status (docs):

@leanprover-bot leanprover-bot added the builds-manual CI has verified that the Lean Language Reference builds against this PR label Dec 9, 2025
@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Dec 9, 2025 •
edited
Loading

Reference manual CI status:

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@digama0 digama0 Awaiting requested review from digama0 digama0 will be requested when the pull request is marked ready for review digama0 is a code owner

@kim-em kim-em Awaiting requested review from kim-em kim-em will be requested when the pull request is marked ready for review kim-em is a code owner

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura will be requested when the pull request is marked ready for review leodemoura is a code owner

@hargoniX hargoniX Awaiting requested review from hargoniX hargoniX will be requested when the pull request is marked ready for review hargoniX is a code owner

Assignees

No one assigned

Labels

breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan builds-manual CI has verified that the Lean Language Reference builds against this PR changelog-language Language features and metaprograms changes-stage0 Contains stage0 changes, merge manually using rebase 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.

grind heterogeneous injectivity vs. parameters

4 participants

@nomeata @leanprover-community-bot @leanprover-bot