Pull requests: leanprover-community/batteries
Author
Label
Projects
Milestones
Reviews
Assignee
Sort
Pull requests list
chore: update This PR is ready for review; the author thinks it is ready to be merged.
make lint to use lake
awaiting-review
#791
opened May 10, 2024 by
semorrison
Loading…
feat: use 'lake test'
awaiting-review
This PR is ready for review; the author thinks it is ready to be merged.
#787
opened May 9, 2024 by
semorrison
Loading…
Add some theorems for 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.
String.substrEq and String.isPrefixOf
awaiting-review
#782
opened May 6, 2024 by
tjf801
Loading…
Add String.length_join and List.length_join
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.
#779
opened May 3, 2024 by
tjf801
Loading…
chore: adaptations for leanprover/lean4#3756
merge-conflict
This PR has merge conflicts with the `main` branch which must be resolved by the author.
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…
feat: 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.
Array.qsort_sorted
awaiting-review
#759
opened Apr 21, 2024 by
digama0
Loading…
refactor: move theorems about lists from mathlib
awaiting-review
This PR is ready for review; the author thinks it is ready to be merged.
#756
opened Apr 19, 2024 by
chabulhwi
Loading…
1 task done
feat: unbundle array size constraint from hash map bucket array (second attempt)
merge-conflict
This PR has merge conflicts with the `main` branch which must be resolved by the author.
feat: This PR has merge conflicts with the `main` branch which must be resolved by the author.
will-merge-soon
PR will be merged soon. Any concerns should be raised quickly.
Rat.toFloat
merge-conflict
#750
opened Apr 18, 2024 by
digama0
Loading…
feat: unbundle array size constraint from hash map bucket array
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.
#748
opened Apr 17, 2024 by
TwoFX
Loading…
2 tasks done
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 Std4 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…
3 of 5 tasks
chore: move RBNode depth lemmas out
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.
#744
opened Apr 16, 2024 by
digama0
Loading…
feat: add This is stacked on top of another Std4 PR.
String.splitOn_of_valid
depends on another PR
#743
opened Apr 16, 2024 by
chabulhwi
Loading…
1 of 2 tasks
feat: RBSet.{upperBound?, lowerBound?} lemmas
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.
#740
opened Apr 14, 2024 by
digama0
Loading…
3 tasks done
feat: RBMap lemmas
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.
#739
opened Apr 13, 2024 by
digama0
Loading…
3 tasks done
feat: fill in proof of Array.erase_data
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.
#690
opened Mar 8, 2024 by
Seppel3210
Loading…
feat: 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.
List.forall_get_iff_forall_mem
awaiting-author
#682
opened Mar 4, 2024 by
Qiu233
Loading…
feat: apply dupNamespace linter to instances
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.
#670
opened Feb 23, 2024 by
Ruben-VandeVelde
Loading…
feat: Fin.powLast
merge-conflict
This PR has merge conflicts with the `main` branch which must be resolved by the author.
WIP
work in progress
#657
opened Feb 17, 2024 by
semorrison
•
Draft
feat: allow writing (0 : Fin (2^n))
merge-conflict
This PR has merge conflicts with the `main` branch which must be resolved by the author.
WIP
work in progress
#656
opened Feb 17, 2024 by
semorrison
•
Draft
feat: add lemma code-action
awaiting-review
This PR is ready for review; the author thinks it is ready to be merged.
#625
opened Feb 12, 2024 by
adomani
Loading…
feat: upstream casesm and cases_type tactics
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.
#597
opened Feb 7, 2024 by
semorrison
Loading…
feat: 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.
List.insertP and lemmas
awaiting-review
#569
opened Jan 30, 2024 by
fgdorais
Loading…
Previous Next
ProTip!
What’s not been updated in a month: updated:<2024-04-10.