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: upstream List.finRange from Batteries #6234

Merged
merged 1 commit into from
Nov 27, 2024
Merged

feat: upstream List.finRange from Batteries #6234

merged 1 commit into from
Nov 27, 2024
+64 −0

Conversation

kim-em
Copy link
Collaborator

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

This PR upstreams the definition and basic lemmas about List.finRange from Batteries.

Thanks for contributors to Batteries and Mathlib who've previously worked on this material. Further PRs are welcome here. I'll be adding more API later.

@kim-em kim-em added the changelog-library Library label Nov 27, 2024
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc November 27, 2024 04:15 Inactive
@kim-em kim-em added this pull request to the merge queue Nov 27, 2024
@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 27, 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 321e148f51eb507acd9bf870ba1a7d469d4ed3b1 --onto 9a17919ef11c2dba824498229633b8333a0b53d9. (2024-11-27 04:31:12)

Merged via the queue into master with commit 7e9dd56 Nov 27, 2024
20 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
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