Skip to content

feat: strengthen finIdxOf? lemmas #8678

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
TwoFX merged 4 commits into from
Jun 11, 2025
Merged

feat: strengthen finIdxOf? lemmas #8678

TwoFX merged 4 commits into from
Jun 11, 2025

Conversation

@eric-wieser
Copy link
Contributor

@eric-wieser eric-wieser commented Jun 8, 2025

This PR makes the LHS of isSome_finIdxOf? and isNone_finIdxOf? more general.

@eric-wieser
feat: strengthen finIdxOf? lemmas
813e86c 
This PR makes the LHS of `isSome_finIdxOf?` and `isNone_finIdxOf?` more general.
@eric-wieser eric-wieser requested a review from kim-em as a code owner June 8, 2025 00:29
@eric-wieser
Copy link
Contributor Author

eric-wieser commented Jun 8, 2025

changelog-library

@github-actions github-actions bot added the changelog-library Library label Jun 8, 2025
@eric-wieser eric-wieser mentioned this pull request Jun 8, 2025
Merged
@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 8, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Jun 8, 2025 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 666fb5c571baa93ec7edf1a7f66d622837632ccb --onto 9b9dd8546a123d746580649b239f26c26d370d20. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-08 01:05:45)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 666fb5c571baa93ec7edf1a7f66d622837632ccb --onto 8422d936cff3b609bd2a1396e82356c82c383386. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-11 07:16:39)

@TwoFX TwoFX self-assigned this Jun 10, 2025
TwoFX
TwoFX reviewed Jun 11, 2025
View reviewed changes
@TwoFX TwoFX added the awaiting-author Waiting for PR author to address issues label Jun 11, 2025
TwoFX
TwoFX approved these changes Jun 11, 2025
View reviewed changes
Copy link
Member

@TwoFX TwoFX left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

@TwoFX TwoFX added this pull request to the merge queue Jun 11, 2025
Merged via the queue into leanprover:master with commit 44e36de Jun 11, 2025
15 checks passed
@leanprover-bot leanprover-bot added the P-medium We may work on this issue if we find the time label Jun 14, 2025
algebraic-dev pushed a commit to algebraic-dev/lean4 that referenced this pull request Jun 18, 2025
@eric-wieser @algebraic-dev
feat: strengthen finIdxOf? lemmas (leanprover#8678)
4bf0e77 
This PR makes the LHS of `isSome_finIdxOf?` and `isNone_finIdxOf?` more
general.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@TwoFX TwoFX TwoFX approved these changes

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

Assignees

@TwoFX TwoFX

Labels

awaiting-author Waiting for PR author to address issues changelog-library Library P-medium We may work on this issue if we find the time 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.

4 participants

@eric-wieser @leanprover-community-bot @TwoFX @leanprover-bot