Skip to content

Pull requests: leanprover-community/batteries

New pull request New
55 Open 1,011 Closed
55 Open 1,011 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
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

chore: remove explicit universes from EStateM results awaiting-review This PR is ready for review; the author thinks it is ready to be merged. builds-mathlib
#1130 opened Feb 10, 2025 by eric-wieser Loading…
3
feat: upstream Equiv breaks-mathlib WIP work in progress
#1126 opened Feb 8, 2025 by fgdorais • Draft
1
feat: add Fin.find?, Fin.findSome? and lemmas awaiting-review This PR is ready for review; the author thinks it is ready to be merged. builds-mathlib
#1099 opened Jan 26, 2025 by fgdorais Loading…
6
feat: add lemmas for List.isPrefixOf? and List.isSuffixOf? awaiting-review This PR is ready for review; the author thinks it is ready to be merged. builds-mathlib
#1098 opened Jan 25, 2025 by fgdorais Loading…
3
feat: add well founded streams awaiting-review This PR is ready for review; the author thinks it is ready to be merged. builds-mathlib
#1079 opened Dec 25, 2024 by fgdorais Loading…
2
feat: add BitVec.ofFn and lemmas awaiting-review This PR is ready for review; the author thinks it is ready to be merged. builds-mathlib
#1078 opened Dec 23, 2024 by fgdorais Loading…
2 tasks done
22
feat: add basic operations for polynomials over GF(2) builds-mathlib WIP work in progress
#1077 opened Dec 22, 2024 by fgdorais • Draft
1
chore: replace Batteries.HashMap with a shim around Std.HashMap builds-mathlib depends on core changes This PR need only be reviewed after changes land in Lean core. merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author.
#1063 opened Nov 24, 2024 by kim-em Loading…
8
refactor: define List.IsChain, deprecate Chain and Chain' awaiting-author Waiting for PR author to address issues breaks-mathlib
#1052 opened Nov 17, 2024 by urkud Loading…
14
fix: add missing initHeartbeats awaiting-author Waiting for PR author to address issues builds-mathlib
#1037 opened Nov 11, 2024 by eric-wieser Loading…
8
feat: add Data.Fin.Coding and Data.Fin.Enum builds-mathlib WIP work in progress
#1007 opened Oct 25, 2024 by fgdorais • Draft
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
#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
feat: dependent array type awaiting-review This PR is ready for review; the author thinks it is ready to be merged. builds-mathlib depends on core changes This PR need only be reviewed after changes land in Lean core.
#813 opened May 27, 2024 by fgdorais Loading…
4
feat: Add String.isPrefixOf theorems awaiting-author Waiting for PR author to address issues
#809 opened May 23, 2024 by tjf801 Loading…
1
chore: upstream Nat.binaryRec awaiting-review This PR is ready for review; the author thinks it is ready to be merged. breaks-mathlib depends on another PR This is stacked on top of another Batteries PR.
#799 opened May 16, 2024 by FR-vdash-bot Loading…
1 task
2
feat: Add String.length_join and List.length_join 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.
#779 opened May 3, 2024 by tjf801 Loading…
5
chore: adaptations for leanprover/lean4#3756 merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. WIP work in progress
#765 opened Apr 24, 2024 by FR-vdash-bot • Draft
1
feat: merging functions on List + mergeSort 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.
#763 opened Apr 23, 2024 by digama0 Loading…
6
feat: Array.qsort_sorted awaiting-review This PR is ready for review; the author thinks it is ready to be merged. merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author.
#759 opened Apr 21, 2024 by digama0 Loading…
4
feat: RBMap lemmas cont'd: find?_erase awaiting-review This PR is ready for review; the author thinks it is ready to be merged. 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.
#745 opened Apr 16, 2024 by digama0 Loading…
5 tasks done
feat: add String.splitOn_of_valid awaiting-review This PR is ready for review; the author thinks it is ready to be merged. 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.
#743 opened Apr 16, 2024 by chabulhwi Loading…
2 tasks done
13
ProTip! Find all pull requests that aren't related to any open issues with -linked:issue.