Pull requests: leanprover-community/batteries
Author
Label
Projects
Milestones
Reviews
Assignee
Sort
Pull requests list
feat: safe Nat indexed Array functions using get_elem_tactic
awaiting-review
This PR is ready for review; the author thinks it is ready to be merged.
#803
opened May 16, 2024 by
Shreyas4991
Loading…
feat: size lemmas for Array.shrink
awaiting-review
This PR is ready for review; the author thinks it is ready to be merged.
#801
opened May 16, 2024 by
Shreyas4991
Loading…
chore: upstream This PR has merge conflicts with the `main` branch which must be resolved by the author.
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
feat: Add some theorems for This PR is ready for review; the author thinks it is ready to be merged.
String.substrEq
and String.isPrefixOf
awaiting-review
#782
opened May 6, 2024 by
tjf801
Loading…
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.
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…
feat: This PR is ready for review; the author thinks it is ready to be merged.
List.insertP
and lemmas
awaiting-review
#569
opened Jan 30, 2024 by
fgdorais
Loading…
WIP: Roadmap document for standard library
awaiting-author
Waiting for PR author to address issues
#561
opened Jan 25, 2024 by
joehendrix
Loading…
Previous Next
ProTip!
Filter pull requests by the default branch with base:main.