Skip to content

Pull requests: leanprover-community/batteries

New pull request New
54 Open 1,261 Closed
54 Open 1,261 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: adaptations for nightly-2025-08-24
#1388 opened Aug 24, 2025 by leanprover-community-mathlib4-bot Loading…
chore: fixed name is_lt_iff_lt to isLT_iff_lt awaiting-review This PR is ready for review; the author thinks it is ready to be merged.
#1387 opened Aug 24, 2025 by qawbecrdtey Loading…
chore: adaptations for nightly-2025-08-21
#1386 opened Aug 21, 2025 by leanprover-community-mathlib4-bot Loading…
chore: adaptations for nightly-2025-08-19 merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author.
#1384 opened Aug 19, 2025 by leanprover-community-mathlib4-bot Loading…
feat: connect streams and iterators awaiting-review This PR is ready for review; the author thinks it is ready to be merged. builds-mathlib
#1372 opened Aug 11, 2025 by fgdorais Loading…
1 task
1
feat: begin using the module system awaiting-review This PR is ready for review; the author thinks it is ready to be merged.
#1362 opened Jul 31, 2025 by kim-em Loading…
2
feat: add Char.all, Char.any and decidability instances awaiting-review This PR is ready for review; the author thinks it is ready to be merged. builds-mathlib
#1344 opened Jul 24, 2025 by fgdorais Loading…
3
feat: add stream combinators awaiting-review This PR is ready for review; the author thinks it is ready to be merged. builds-mathlib
#1334 opened Jul 20, 2025 by fgdorais Loading…
1 task
1
feat: coding functions for Fin awaiting-review This PR is ready for review; the author thinks it is ready to be merged. builds-mathlib
#1332 opened Jul 19, 2025 by fgdorais Loading…
9
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
#1331 opened Jul 18, 2025 by fgdorais Loading…
2
feat: add @[simp] lemma WellFounded.val_wrap awaiting-review This PR is ready for review; the author thinks it is ready to be merged. breaks-mathlib
#1308 opened Jul 1, 2025 by plp127 Loading…
13
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
3
feat: fix some issues with equals t => tac awaiting-author Waiting for PR author to address issues builds-mathlib
#1291 opened Jun 26, 2025 by plp127 Loading…
2
feat: add case insensitive comparison for strings (ASCII only) awaiting-author Waiting for PR author to address issues breaks-mathlib
#1283 opened Jun 18, 2025 by ammkrn Loading…
18
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
feat: redefinition of Float functions using axioms and proofs about Float WIP work in progress
#1141 opened Feb 19, 2025 by Rob23oba • Draft
refactor: define List.IsChain, deprecate Chain and Chain' awaiting-author Waiting for PR author to address issues breaks-mathlib merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author.
#1052 opened Nov 17, 2024 by urkud Loading…
15
fix: add missing initHeartbeats awaiting-author Waiting for PR author to address issues builds-mathlib
#1037 opened Nov 11, 2024 by eric-wieser Loading…
10
feat: add Data.Fin.Enum builds-mathlib merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. WIP work in progress
#1007 opened Oct 25, 2024 by fgdorais • Draft
1 task
18
feat: add List.commonPrefix and its lemmas awaiting-author Waiting for PR author to address issues
#994 opened Oct 16, 2024 by chabulhwi Loading…
9
feat: add list function and lemmas awaiting-author Waiting for PR author to address issues merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author.
#987 opened Oct 14, 2024 by chabulhwi Loading…
34
feat: the trailingWhitespace linter awaiting-review This PR is ready for review; the author thinks it is ready to be merged. builds-mathlib
#920 opened Aug 16, 2024 by adomani Loading…
6
feat: order lemmas for UIntX types 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.
#854 opened Jun 20, 2024 by fgdorais Loading…
8
feat: folds for dependent arrays depends on another PR This is stacked on top of another Batteries PR. merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. WIP work in progress
#815 opened May 29, 2024 by fgdorais • Draft
2 of 3 tasks
ProTip! Follow long discussions with comments:>50.