Skip to content
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

fix: avoid nonexistent noConfusions in injection, contradiction #6731

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

fix: avoid nonexistent noConfusions in injection, contradiction #6731

wants to merge 1 commit into from
+70 −4

Conversation

jrr6
Copy link
Contributor

@jrr6 jrr6 commented Jan 21, 2025

This PR fixes an issue where injection and contradiction would attempt to apply nonexistent no-confusion principles.

Closes #6515.

@jrr6 jrr6 force-pushed the contradiction-disjunction branch from 6fcce8f to a4d60c9 Compare January 21, 2025 20:04
@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 Jan 21, 2025
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase eb30249b1118b5bea767354d5362f4afba97c82e --onto f9e904af5022a57adb6105cda65d1569449346c2. (2025-01-21 20:38:59)

@jrr6 jrr6 added the changelog-language Language features, tactics, and metaprograms label Jan 21, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@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

Assignees
No one assigned
Labels
changelog-language Language features, tactics, and metaprograms 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.

contradiction tries to make use of constructor disjunction for proof equalities
2 participants
@jrr6 @leanprover-community-bot