Skip to content

feat: Extend the API of findIdxs and idxsOf #1500

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
fgdorais merged 26 commits into from
Nov 24, 2025
Merged

feat: Extend the API of findIdxs and idxsOf #1500

fgdorais merged 26 commits into from
Nov 24, 2025

Conversation

@linesthatinterlace
Copy link
Contributor

@linesthatinterlace linesthatinterlace commented Nov 7, 2025 •
edited
Loading

This PR improves the API for List.indexesOf and List.findIdxs.

This depends on #1506. This is depended on by #1507

@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 Nov 7, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Nov 7, 2025
@leanprover-community-mathlib4-bot
Update Batteries branch for testing leanprover-community/batteries#1500
0ab39bf
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Nov 7, 2025 •
edited
Loading

Mathlib CI status (docs):

eric-wieser
eric-wieser reviewed Nov 7, 2025
View reviewed changes
fgdorais
fgdorais requested changes Nov 8, 2025
View reviewed changes
@linesthatinterlace linesthatinterlace force-pushed the idxsOf branch 2 times, most recently from d62488a to ecfd677 Compare November 10, 2025 10:03
eric-wieser
eric-wieser reviewed Nov 10, 2025
View reviewed changes
eric-wieser
eric-wieser reviewed Nov 10, 2025
View reviewed changes
@eric-wieser
Copy link
Member

eric-wieser commented Nov 10, 2025

c) This allows us to prove (with minimal labour - i.e. automation is handling most of it!) a neat enumeration result between indices of a list and the collection of elements with their counts.

I think this would be best split to a separate PR.

@linesthatinterlace
Copy link
Contributor Author

linesthatinterlace commented Nov 10, 2025

Agreed re: separate PR. I am currently working on splitting this one out. See #1506 which focuses on the name change.

@linesthatinterlace
Copy link
Contributor Author

linesthatinterlace commented Nov 10, 2025

Please ignore my force pushes above - I was trying to rebase onto #1506 and I think something badly messed up.

This was referenced Nov 10, 2025
Open
Merged
eric-wieser
eric-wieser reviewed Nov 10, 2025
View reviewed changes
eric-wieser
eric-wieser reviewed Nov 10, 2025
View reviewed changes
eric-wieser
eric-wieser reviewed Nov 10, 2025
View reviewed changes
eric-wieser
eric-wieser reviewed Nov 10, 2025
View reviewed changes
eric-wieser
eric-wieser reviewed Nov 10, 2025
View reviewed changes
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Nov 10, 2025
@linesthatinterlace
Copy link
Contributor Author

linesthatinterlace commented Nov 11, 2025

It's possible we should change the if in findIdxsValues to bif - there is some inconsistency about this in the library in general I think but I think bif is more common.

@linesthatinterlace linesthatinterlace changed the title feat: Extend the API of findIdxs and idxsOf and add enumeration functions. feat: Extend the API of findIdxs and idxsOf Nov 12, 2025
fgdorais
fgdorais reviewed Nov 13, 2025
View reviewed changes
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Nov 18, 2025
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Nov 18, 2025
fgdorais
fgdorais requested changes Nov 22, 2025
View reviewed changes
Copy link
Collaborator

@fgdorais fgdorais left a comment

Choose a reason for hiding this comment

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

Please update the docstrings with examples and document the use of start.

@fgdorais fgdorais mentioned this pull request Nov 24, 2025
Closed
4 tasks
@fgdorais fgdorais added this pull request to the merge queue Nov 24, 2025
Merged via the queue into leanprover-community:main with commit 2688408 Nov 24, 2025
1 check passed
@github-actions github-actions bot removed the awaiting-review This PR is ready for review; the author thinks it is ready to be merged. label Nov 24, 2025
mathlib-bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Nov 25, 2025
@fgdorais @leanprover-community-mathlib4-bot @linesthatinterlace
chore: adaptation for batteries#1500 (#32075)
7bf950c 
After [batteries#1500](leanprover-community/batteries#1500) is merged:

- [x] Edit the lakefile to point to leanprover-community/batteries:main
- [x] Run lake update batteries
- [x] Merge leanprover-community/mathlib4:master
- [ ] Wait for CI and merge

Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Wrenna Robson <[email protected]>
Co-authored-by: F. G. Dorais <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@fgdorais fgdorais fgdorais approved these changes

Assignees

No one assigned

Labels

builds-mathlib

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@linesthatinterlace @leanprover-community-bot @eric-wieser @fgdorais @leanprover-community-mathlib4-bot