Skip to content

Issues: leanprover/lean4

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Clear current search query, filters, and sorts
27 Open 474 Closed
27 Open 474 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
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
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

feat: grind attributes for relation typeclasses changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8459 opened May 24, 2025 by kim-em • Draft
2
feat: introduce iterator combinators filterMap, filter and map changelog-library Library
#8451 opened May 23, 2025 by datokrat • Draft
feat: upstream LawfulMonadLift(T) from Batteries builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8435 opened May 21, 2025 by datokrat Loading…
14
feat: introduce drop iterator combinator changelog-library Library
#8420 opened May 20, 2025 by datokrat • Draft
feat: introduce take iterator combinator builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8418 opened May 20, 2025 by datokrat • Draft
1
feat: Add getElem_swapIfInBounds* lemmas and deprecate getElem_swap' changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8406 opened May 19, 2025 by linesthatinterlace Loading…
3
feat: ForIn, fold(M), drain lemmas for iterators builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8405 opened May 19, 2025 by datokrat Loading…
1
feat: equivalence of tree maps awaiting-review Waiting for someone to review the PR changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8210 opened May 2, 2025 by Rob23oba • Draft
@TwoFX
3
feat: simplify T-division into E-division when numerator is positive builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library P-medium We may work on this issue if we find the time toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8205 opened May 2, 2025 by bollu Loading…
3
feat: characterize when T-division equals zero builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library P-medium We may work on this issue if we find the time toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8204 opened May 2, 2025 by bollu Loading…
4
feat: Bitvector trichotomy lemmas builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library P-medium We may work on this issue if we find the time toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8203 opened May 2, 2025 by bollu Loading…
8
feat: add system information functions to the standard library changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8109 opened Apr 25, 2025 by algebraic-dev Loading…
1
feat: add DNS resolution functions to the standard library changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8072 opened Apr 23, 2025 by algebraic-dev Loading…
1
feat: BaseIO.joinTask builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8070 opened Apr 23, 2025 by tydeu • Draft
7
feat: monadic interface for asynchronous operations in Std changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8003 opened Apr 17, 2025 by algebraic-dev Loading…
15
feat: some Option.filter lemmas builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7820 opened Apr 4, 2025 by TwoFX • Draft
1
feat: Constructions for splitting and merging vectors of bitvectors changelog-library Library P-medium We may work on this issue if we find the time toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN WIP This is work in progress, and only a PR for the sake of CI or sharing. No review yet.
#7754 opened Mar 31, 2025 by javra Loading…
10
chore: add BitVec.(toNat, toInt, toFin)_shiftLeftZeroExtend changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7662 opened Mar 24, 2025 by luisacicolini • Draft
8
feat: add min and max to seval changelog-library Library P-low We are not planning to work on this issue toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7464 opened Mar 13, 2025 by bollu Loading…
10
feat: Nat.dfold builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7450 opened Mar 12, 2025 by kim-em Loading…
1
fix: inline Nat.cast changelog-library Library P-low We are not planning to work on this issue toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7283 opened Mar 1, 2025 by eric-wieser Loading…
6
feat: Confluent simp-set for left shift by BitVec.twoPow builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6782 opened Jan 26, 2025 by bollu • Draft
3
feat: Nat.decidableBallLT handles large numbers awaiting-author Waiting for PR author to address issues builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library P-medium We may work on this issue if we find the time stale toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6651 opened Jan 15, 2025 by llllvvuu Loading…
16
feat: define Squash as a Quotient awaiting-author Waiting for PR author to address issues awaiting-mathlib We should not merge this until we have a successful Mathlib build breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-library Library stale toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6642 opened Jan 14, 2025 by vihdzp Loading…
10
feat: runtime primitives for mpz objects awaiting-author Waiting for PR author to address issues builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library stale toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6395 opened Dec 16, 2024 by tydeu • Draft
8
ProTip! Add no:assignee to see everything that’s not assigned.