-
Notifications
You must be signed in to change notification settings - Fork 84
Pull requests: leanprover-community/batteries
Author
Label
Projects
Milestones
Reviews
Assignee
Sort
Pull requests list
feat: Add This PR is ready for review; the author thinks it is ready to be merged.
String.isPrefixOf
theorems
awaiting-review
#809
opened May 23, 2024 by
tjf801
Loading…
refactor: make work in progress
List.length_eq_countP_add_countP
avoid Prop
WIP
#808
opened May 23, 2024 by
BoltonBailey
Loading…
feat: size lemma for This PR is ready for review; the author thinks it is ready to be merged.
Array.set!
awaiting-review
#807
opened May 23, 2024 by
fgdorais
Loading…
chore: upstream This PR has merge conflicts with the `main` branch which must be resolved by the author.
WIP
work in progress
Nat.binaryRec
merge-conflict
chore: align This PR is ready for review; the author thinks it is ready to be merged.
will-merge-soon
PR will be merged soon. Any concerns should be raised quickly.
isInternalName
with upstream version
awaiting-review
#796
opened May 14, 2024 by
semorrison
Loading…
feat: statically sized Vector type
awaiting-review
This PR is ready for review; the author thinks it is ready to be merged.
#793
opened May 11, 2024 by
Shreyas4991
Loading…
1 task done
feat: Add 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.length_join
and List.length_join
awaiting-review
#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.
WIP
work in progress
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: 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
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: 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-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.
#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…
Previous Next
ProTip!
Type g p on any issue or pull request to go back to the pull request listing page.