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: add Fin.find? and lemmas #1099

Open
wants to merge 2 commits into
base: main
Choose a base branch
from
Open

feat: add Fin.find? and lemmas #1099

wants to merge 2 commits into from
+87 −0

Conversation

fgdorais
Copy link
Collaborator

No description provided.

@github-actions github-actions bot added the awaiting-review This PR is ready for review; the author thinks it is ready to be merged. label Jan 26, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 26, 2025
@leanprover-community-mathlib4-bot
Update Batteries branch for testing leanprover-community/batteries#1099
ddc6ce8
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Jan 26, 2025 •
edited
Loading

Mathlib CI status (docs):

kim-em
kim-em reviewed Jan 30, 2025
View reviewed changes
Batteries/Data/Fin/Lemmas.lean Outdated

theorem find?_isNone {f : Fin n → Option α} : (find? f).isNone ↔ ∀ i, (f i).isNone := by simp

theorem find?_eq_list_join_find?_ofFn_isSome {f : Fin n → Option α} :
Copy link
Collaborator

Choose a reason for hiding this comment

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

What about the other lemma, saying l.find? f = Fin.find? (fun (i : Fin l.length) => f l[i])?

Copy link
Collaborator Author

@fgdorais fgdorais Jan 30, 2025 •
edited
Loading

Choose a reason for hiding this comment

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

On it... might take a day or so...

@fgdorais @kim-em
fix: naming convention
b198ae5 
Co-authored-by: Kim Morrison <[email protected]>
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 30, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover-community/batteries#1099
4368e7a
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kim-em kim-em kim-em left review comments

Assignees
No one assigned
Labels
awaiting-review This PR is ready for review; the author thinks it is ready to be merged. builds-mathlib
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@fgdorais @leanprover-community-bot @kim-em