Skip to content

Pull requests: leanprover-community/batteries

New pull request New
57 Open 1,722 Closed
57 Open 1,722 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: remove the checkUnivs linter awaiting-review This PR is ready for review; the author thinks it is ready to be merged. builds-mathlib
#1864 opened Jun 19, 2026 by grunweg Contributor Loading…
2
chore: remove the defLemma linter awaiting-review This PR is ready for review; the author thinks it is ready to be merged. builds-mathlib
#1863 opened Jun 19, 2026 by grunweg Contributor Loading…
3
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(Tactic): upstream @[mk_iff] from mathlib awaiting-review This PR is ready for review; the author thinks it is ready to be merged. breaks-mathlib
#1854 opened Jun 15, 2026 by YaelDillies Contributor Loading…
19
feat(Data): interleaving lists awaiting-review This PR is ready for review; the author thinks it is ready to be merged. breaks-mathlib
#1853 opened Jun 15, 2026 by YaelDillies Contributor Loading…
24
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…
8
chore: use core checks/error messages in the env_linter attribute awaiting-review This PR is ready for review; the author thinks it is ready to be merged. builds-mathlib
#1837 opened Jun 3, 2026 by chenson2018 Loading…
6
feat: isPrivateOrAutoDecl awaiting-review This PR is ready for review; the author thinks it is ready to be merged. builds-mathlib
#1835 opened Jun 2, 2026 by thorimur Contributor Loading…
4
fix: don't consider private names autogenerated in isAutoDecl breaks-mathlib WIP work in progress
#1831 opened Jun 2, 2026 by thorimur Contributor • Draft
1 task
6
chore: rename type class linter awaiting-review This PR is ready for review; the author thinks it is ready to be merged. breaks-mathlib
#1830 opened Jun 1, 2026 by fgdorais Collaborator Loading…
3
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…
7
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…
2
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 awaiting-review This PR is ready for review; the author thinks it is ready to be merged. breaks-mathlib
#1727 opened Mar 20, 2026 by thorimur Contributor Loading…
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
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 Contributor Loading…
3
ProTip! Exclude everything labeled bug with -label:bug.