Skip to content

Pull requests: leanprover-community/batteries

New pull request New
52 Open 1,515 Closed
52 Open 1,515 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Reviews
Filter by reviews
No reviews Review required Approved review Changes requested
Assignee
Filter by who’s assigned
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

chore: migrate nightly-testing workflows to GitHub App awaiting-review This PR is ready for review; the author thinks it is ready to be merged.
#1652 opened Feb 3, 2026 by kim-em Loading…
1
chore: migrate merge-conflicts workflow to GitHub App awaiting-review This PR is ready for review; the author thinks it is ready to be merged. builds-mathlib
#1651 opened Feb 3, 2026 by kim-em Loading…
1
perf: use Thunk in NameMapExtension breaks-mathlib WIP work in progress
#1650 opened Feb 2, 2026 by JovanGerb Loading…
1
[WIP] feat: port SatisfiesM lemmas to mvcgen WIP work in progress
#1649 opened Feb 2, 2026 by cmlsharp • Draft
1
fix: don't re-export everything every time in batteriesLinterExt awaiting-review This PR is ready for review; the author thinks it is ready to be merged. builds-mathlib
#1648 opened Feb 2, 2026 by JovanGerb Loading…
1
perf(Tactic/Alias): use MapDeclarationExtension awaiting-review This PR is ready for review; the author thinks it is ready to be merged. builds-mathlib
#1646 opened Feb 2, 2026 by JovanGerb Loading…
3
feat: scan combinators for Vectors awaiting-review This PR is ready for review; the author thinks it is ready to be merged. builds-mathlib
#1643 opened Jan 30, 2026 by cmlsharp Loading…
1
feat: add List1 type builds-mathlib on-hiatus This PR will not be merged soon but it may be reconsidered later if need arises.
#1609 opened Jan 7, 2026 by Rob23oba • Draft
2
feat: nonempty list type builds-mathlib on-hiatus This PR will not be merged soon but it may be reconsidered later if need arises.
#1607 opened Jan 7, 2026 by fgdorais • Draft
3
feat: support simp?/simp_all?/dsimp? in squeeze_scope awaiting-review This PR is ready for review; the author thinks it is ready to be merged.
#1604 opened Jan 6, 2026 by kim-em Loading…
Verification of binary heap awaiting-review This PR is ready for review; the author thinks it is ready to be merged. builds-mathlib
#1602 opened Jan 6, 2026 by cmlsharp Loading…
10
fix: correct behavior of runLinter --update builds-mathlib merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. WIP work in progress
#1600 opened Jan 5, 2026 by thorimur Loading…
3
feat: add Alternative.{many,many1} awaiting-author Waiting for PR author to address issues builds-mathlib merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author.
#1595 opened Jan 3, 2026 by 414owen Loading…
1
35
feat: add scan combinator for iterators awaiting-review This PR is ready for review; the author thinks it is ready to be merged. builds-mathlib
#1590 opened Dec 31, 2025 by cmlsharp Loading…
12
feat: Add Array.scan{l,r,lM,rM} awaiting-review This PR is ready for review; the author thinks it is ready to be merged. builds-mathlib will-merge-soon PR will be merged soon. Any concerns should be raised quickly.
#1589 opened Dec 31, 2025 by cmlsharp Loading…
55
feat: List.getElem_flatten awaiting-review This PR is ready for review; the author thinks it is ready to be merged. builds-mathlib
#1511 opened Nov 12, 2025 by kim-em Loading…
1 task done
4
feat: Add enumeration between list indicies and element-multiplicity pairs. awaiting-review This PR is ready for review; the author thinks it is ready to be merged. builds-mathlib
#1507 opened Nov 10, 2025 by linesthatinterlace Loading…
12
feat: add Fin.any and Fin.all awaiting-review This PR is ready for review; the author thinks it is ready to be merged. builds-mathlib
#1435 opened Sep 29, 2025 by fgdorais Loading…
10
feat: add stream combinators awaiting-review This PR is ready for review; the author thinks it is ready to be merged. builds-mathlib merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author.
#1334 opened Jul 20, 2025 by fgdorais Loading…
1 task
1
feat: coding functions for Fin builds-mathlib WIP work in progress
#1332 opened Jul 19, 2025 by fgdorais Loading…
1 task done
54
feat: add finite and well-founded streams awaiting-review This PR is ready for review; the author thinks it is ready to be merged. builds-mathlib merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author.
#1331 opened Jul 18, 2025 by fgdorais Loading…
3
feat: add Nat.Digits merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. WIP work in progress
#1293 opened Jun 26, 2025 by fgdorais • Draft
6
feat: fix some issues with equals t => tac awaiting-review This PR is ready for review; the author thinks it is ready to be merged. builds-mathlib
#1291 opened Jun 26, 2025 by plp127 Loading…
4
fix: use getRel in @[trans] attribute awaiting-author Waiting for PR author to address issues breaks-mathlib help wanted Extra attention is needed
#1223 opened May 4, 2025 by digama0 Loading…
1
8
implement List.max! and List.min! awaiting-author Waiting for PR author to address issues builds-mathlib
#1174 opened Mar 24, 2025 by Seasawher Loading…
2
ProTip! no:milestone will show everything without a milestone.