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

feat: lemmas for Array.findSome? and find? #6111

Merged
merged 10 commits into from
Nov 18, 2024
Merged

feat: lemmas for Array.findSome? and find? #6111

merged 10 commits into from
Nov 18, 2024

Conversation

kim-em
Copy link
Collaborator

@kim-em kim-em commented Nov 18, 2024 •
edited
Loading

This PR fills in the API for Array.findSome? and Array.find?, transferring proofs from the corresponding List statements.

@kim-em kim-em requested a review from digama0 as a code owner November 18, 2024 03:44
@kim-em kim-em added the changelog-library Library label Nov 18, 2024
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc November 18, 2024 04:05 Inactive
@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 Nov 18, 2024
@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 62ae320e1cab66b394ff96d01bb90335e325e3fd --onto a074bd9a2bd20cc470fbff4f80f2cd7b51ec0d0a. (2024-11-18 04:06:37)

@kim-em kim-em added this pull request to the merge queue Nov 18, 2024
Merged via the queue into master with commit e10fac9 Nov 18, 2024
18 of 20 checks passed
JovanGerb pushed a commit to JovanGerb/lean4 that referenced this pull request Jan 21, 2025
@kim-em @JovanGerb
feat: lemmas for Array.findSome? and find? (leanprover#6111)
d4474d9 
This PR fills in the API for `Array.findSome?` and `Array.find?`,
transferring proofs from the corresponding List statements.
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 is a code owner

Assignees
No one assigned
Labels
changelog-library Library 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.
2 participants
@kim-em @leanprover-community-bot