Skip to content

Pull requests: leanprover-community/batteries

New pull request New
58 Open 1,759 Closed
58 Open 1,759 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

perf(lint): collect fvars once in impossibleInstance and explicitVarsOfIff awaiting-review This PR is ready for review; the author thinks it is ready to be merged. builds-mathlib
#1894 opened Jul 9, 2026 by marcelolynch Contributor Loading…
1
fix: ignore synthetic match terms in matchExpand code action awaiting-review This PR is ready for review; the author thinks it is ready to be merged. builds-mathlib
#1893 opened Jul 8, 2026 by Chessing234 Loading…
1 of 2 tasks
1
1
chore: ignore deprecated declarations in some linters awaiting-review This PR is ready for review; the author thinks it is ready to be merged. builds-mathlib
#1892 opened Jul 7, 2026 by thorimur Contributor Loading…
9
feat(runLinter): --profile to report the slowest checks per linter builds-mathlib WIP work in progress
#1890 opened Jul 7, 2026 by marcelolynch Contributor Loading…
1
chore: deprecate MLList in favour of Std.IterM WIP work in progress
#1887 opened Jul 5, 2026 by Seasawher Contributor • Draft
perf: make a List.filter grind annotation less aggressive awaiting-review This PR is ready for review; the author thinks it is ready to be merged. breaks-mathlib
#1880 opened Jun 25, 2026 by hargoniX Contributor Loading…
4
chore: shake breaks-mathlib merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. WIP work in progress
#1872 opened Jun 21, 2026 by fgdorais Collaborator Loading…
9
feat: flesh out def_wanted / ❰…❱ references (universes, transitive deps, transparency) awaiting-review This PR is ready for review; the author thinks it is ready to be merged.
#1861 opened Jun 18, 2026 by kim-em Collaborator Loading…
2
feat: consume lake target specs in runLinter awaiting-review This PR is ready for review; the author thinks it is ready to be merged. builds-mathlib
#1850 opened Jun 11, 2026 by eric-wieser Member Loading…
12
feat: don't consider private names autogenerated in isAutoDecl awaiting-review This PR is ready for review; the author thinks it is ready to be merged. builds-mathlib
#1831 opened Jun 2, 2026 by thorimur Contributor Loading…
3 of 4 tasks
17
refactor: consolidate linters 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.
#1830 opened Jun 1, 2026 by fgdorais Collaborator Loading…
23
feat: add tape data structure awaiting-review This PR is ready for review; the author thinks it is ready to be merged. builds-mathlib
#1815 opened May 23, 2026 by fgdorais Collaborator Loading…
8
feat: add basic byte order support breaks-mathlib WIP work in progress
#1811 opened May 18, 2026 by fgdorais Collaborator Loading…
18
Added 15 backward.simpa.using.reducibleClose merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author.
#1797 opened May 7, 2026 by Deicyde Loading…
1
[WIP] feat(UnionFind): add construction witness WIP work in progress
#1761 opened Apr 7, 2026 by Oppen • Draft
chore: cleanup grind attributes awaiting-review This PR is ready for review; the author thinks it is ready to be merged. breaks-mathlib
#1744 opened Mar 31, 2026 by kim-em Collaborator Loading…
3
Upstreaming bit, div2, bodd and establishing binary recursion. breaks-mathlib WIP work in progress
#1737 opened Mar 26, 2026 by wrenna-robson Contributor Loading…
33
chore: upstream Nat.binaryRec awaiting-review This PR is ready for review; the author thinks it is ready to be merged. breaks-mathlib
#1730 opened Mar 23, 2026 by astrainfinita Contributor Loading…
fix: update defLemma and related linters correctly breaks-mathlib merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. WIP work in progress
#1727 opened Mar 20, 2026 by thorimur Contributor • Draft
4
feat: limit the use of Classical.choice merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. no-action There is no need to act on this
#1698 opened Feb 24, 2026 by riccardobrasca Member • Draft
2
perf: run linters only on public imports awaiting-author Waiting for PR author to address issues breaks-mathlib
#1688 opened Feb 21, 2026 by JovanGerb Contributor Loading…
2
perf: tweak runLinter WIP work in progress
#1668 opened Feb 12, 2026 by thorimur Contributor • Draft
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 Contributor • 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 Collaborator • Draft
3
feat: 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 Contributor Loading…
19
ProTip! Mix and match filters to narrow down what you’re looking for.