Skip to content

Pull requests: leanprover/lean4

New pull request New
194 Open 4,453 Closed
194 Open 4,453 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

feat: align {List/Array/Vector}.{foldl, foldr, foldlM, foldrM} lemmas changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6707 opened Jan 20, 2025 by kim-em • Queued
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
feat: complete alignment of {List,Array,Vector}.{mapIdx,mapFinIdx} changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6701 opened Jan 20, 2025 by kim-em • Queued
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
fix: don't generate code for decls with an implemented_by attribute builds-mathlib CI has verified that Mathlib builds against this PR changelog-compiler Compiler, runtime, and FFI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6680 opened Jan 17, 2025 by zwarich Loading…
2
fix: allow ⱼ in identifiers 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
#6679 opened Jan 17, 2025 by hargoniX Loading…
2
feat: add proper erasure of type dependencies in LCNF builds-mathlib CI has verified that Mathlib builds against this PR changelog-compiler Compiler, runtime, and FFI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6678 opened Jan 17, 2025 by zwarich Loading…
1
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: add BitVec.[getMsbD_mul, getElem_udiv, getLsbD_udiv, getMsbD_udiv] 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
#6674 opened Jan 16, 2025 by luisacicolini Loading…
6
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
fix: negative timestamps and PlainDateTimes before 1970 changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6668 opened Jan 16, 2025 by algebraic-dev Loading…
@algebraic-dev
1
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…
43
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
ProTip! Filter pull requests by the default branch with base:master.