Skip to content

Pull requests: leanprover/lean4

New pull request New
190 Open 4,466 Closed
190 Open 4,466 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: disable Elab.async on the cmdline for now toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6722 opened Jan 21, 2025 by Kha Loading…
3
feat: add BitVec multiplication simp lemmas toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6718 opened Jan 20, 2025 by vlad902 Loading…
6
feat: support UIntX and USize in bv_decide changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6711 opened Jan 20, 2025 by hargoniX • Draft
1
feat: make core app unexpanders tag tokens changelog-pp Pretty printing toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6704 opened Jan 20, 2025 by kmill Loading…
2
feat: modify delaborator to tag generalized field notation changelog-pp Pretty printing toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6703 opened Jan 20, 2025 by kmill Loading…
1
perf: avoid lock on deallocating finished tasks toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6699 opened Jan 19, 2025 by Kha • Draft
3
feat: TCP socket support using LibUV
#6683 opened Jan 17, 2025 by algebraic-dev • Draft
10
doc: clarify that lean_initialize_runtime_module is implied by lean_initialize builds-mathlib CI has verified that Mathlib builds against this PR toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6677 opened Jan 17, 2025 by eric-wieser Loading…
1
feat: do not report metaprogramming declarations via exact? and rw? changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6672 opened Jan 16, 2025 by kim-em Loading…
8
feat: Nat.decidableBallLT handles large numbers awaiting-review Waiting for someone to review the PR 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
#6651 opened Jan 15, 2025 by llllvvuu Loading…
13
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 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: allow updating binders to and from strict- and instance-implicit builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6634 opened Jan 14, 2025 by jrr6 Loading…
1
3
feat: add SMT-LIB overflow definitions for bitvectors (not_overflow,uadd_overflow,sadd_overflow,umul_overflow,smul_overflow) 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
#6628 opened Jan 13, 2025 by luisacicolini • Draft
5
feat: lemmas for HashMap.alter and .modify 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
#6620 opened Jan 13, 2025 by datokrat Loading…
59
perf: use C23's free_sized when available toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6598 opened Jan 10, 2025 by eric-wieser Loading…
5
feat: allow more Unicode characters in identifiers builds-mathlib CI has verified that Mathlib builds against this PR toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6579 opened Jan 8, 2025 by thejohncrafter • Draft
1 of 2 tasks
1
2
fix: reduce Eq.rec when mvars are present builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features, tactics, and metaprograms 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
#6577 opened Jan 8, 2025 by cppio Loading…
1
4
fix: respect explicitly inaccessible pattern variables builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features, tactics, and metaprograms 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
#6558 opened Jan 7, 2025 by cppio Loading…
1
4
docs: msys2: leaving a helpful note toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6552 opened Jan 6, 2025 by Kreijstal • Draft
1
fix: don't treat non-atomic idents as pattern variables builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features, tactics, and metaprograms 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
#6551 opened Jan 6, 2025 by cppio Loading…
1
2
chore: add regression test for issue 5925 builds-mathlib CI has verified that Mathlib builds against this PR changelog-no Do not include this PR in the release changelog toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6511 opened Jan 2, 2025 by kmill • Draft
1
feat: bv_decide short-circuit a * x = b * x 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
#6496 opened Jan 1, 2025 by tobiasgrosser Loading…
3
fix: make sure #guard_* uses syntactic equality breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6483 opened Dec 31, 2024 by kmill Loading…
1
feat: add Bitvec reverse definition, getLsbD_reverse, getMsbD_reverse, reverse_append, reverse_replicate and Nat.mod_sub_eq_sub_mod changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN will-merge-soon …unless someone speaks up
#6476 opened Dec 30, 2024 by luisacicolini Loading…
33
perf: tune Array.push runtime code toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6471 opened Dec 29, 2024 by hargoniX • Draft
5
ProTip! Find all pull requests that aren't related to any open issues with -linked:issue.