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?, Fin.findMap? and lemmas #1099

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

feat: add Fin.find?, Fin.findMap? and lemmas #1099

wants to merge 12 commits into from
+248 −0

Conversation

fgdorais
Copy link
Collaborator

@fgdorais fgdorais commented Jan 26, 2025 •
edited
Loading

@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):

@fgdorais @kim-em
fix: naming convention
b198ae5 
Co-authored-by: Kim Morrison <kim@tqft.net>
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
@fgdorais fgdorais added WIP work in progress and removed awaiting-review This PR is ready for review; the author thinks it is ready to be merged. labels Jan 30, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 31, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover-community/batteries#1099
eca9084
@fgdorais fgdorais changed the title feat: add Fin.find? and lemmas feat: add Fin.find?, Fin.findMap? and lemmas Jan 31, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 1, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover-community/batteries#1099
31dc358
@fgdorais fgdorais added the depends on another PR This is stacked on top of another Batteries PR. label Feb 1, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 1, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover-community/batteries#1099
0c15986
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 1, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover-community/batteries#1099
f0460b3
@fgdorais fgdorais added awaiting-review This PR is ready for review; the author thinks it is ready to be merged. and removed WIP work in progress labels Feb 1, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 1, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover-community/batteries#1099
2030547
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 depends on another PR This is stacked on top of another Batteries PR.
Projects
None yet
Milestone
No milestone
Development

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