Skip to content

Pull requests: leanprover/lean4

New pull request New
324 Open 7,804 Closed
324 Open 7,804 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
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

feat: verify all and any for hash maps
#10765 opened Oct 13, 2025 by jt0202 • Draft
fix: avoid unnecessary branching in match compilation breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#10763 opened Oct 13, 2025 by nomeata • Draft
1
2
fix: detect private references in inferred type of public def changelog-no Do not include this PR in the release changelog
#10762 opened Oct 13, 2025 by Kha Loading…
feat: hash map 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
#10761 opened Oct 13, 2025 by datokrat • Draft
2
refactor: remove the second elim dead branches pass toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#10759 opened Oct 13, 2025 by hargoniX • Draft
4
chore: remove redundant imports in core toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#10750 opened Oct 12, 2025 by Kha Loading…
5
fix: Rename theorems that use sorted instead of pairwise awaiting-review Waiting for someone to review the PR toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#10743 opened Oct 11, 2025 by linesthatinterlace • Draft
1
4
feat: add instances NeZero(n^0) for n : Nat and n : Int toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#10739 opened Oct 10, 2025 by fgdorais Loading…
3
fix: hovers and docstrings for (co)inductive types changelog-server Language server, widgets, and IDE extensions toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#10738 opened Oct 10, 2025 by david-christiansen Loading…
5
chore: prepare for cleaning up String namespace 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
#10735 opened Oct 10, 2025 by TwoFX • Draft
2
feat: flatMap 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
#10728 opened Oct 9, 2025 by datokrat Loading…
3
fix: make name mangling unambiguous changelog-compiler Compiler, runtime, and FFI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#10727 opened Oct 9, 2025 by Rob23oba Loading…
1
2
chore: even more module system fixes and refinements from Mathlib porting builds-manual CI has verified that the Lean Language Reference builds against this PR 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
#10726 opened Oct 9, 2025 by Kha Loading…
2
refactor: use Shrink stub in the iterator framework 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
#10725 opened Oct 9, 2025 by datokrat Loading…
15
fix: consider underscores in getHexNumSize changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#10719 opened Oct 8, 2025 by Rob23oba Loading…
2
fix: do not crash in mkAuxTheorem builds-manual CI has verified that the Lean Language Reference builds against this PR builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#10704 opened Oct 7, 2025 by eric-wieser Loading…
5
feat: TreeMap iterators changelog-library Library
#10703 opened Oct 7, 2025 by datokrat • Draft
1 of 7 tasks
1
fix: allow interdependent fvars and mvars in mkAuxTheorem
#10702 opened Oct 7, 2025 by eric-wieser • Draft
1
2
fix: preserve more information through liftCommandElabM changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#10675 opened Oct 5, 2025 by Rob23oba Loading…
1
2
feat: adds acceptSelector and modified selectors changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#10667 opened Oct 3, 2025 by algebraic-dev Loading…
@algebraic-dev
22
chore: shake Init
#10659 opened Oct 2, 2025 by Kha • Draft
7
fix: make .congr_simp theorems private changelog-no Do not include this PR in the release changelog
#10656 opened Oct 2, 2025 by Kha • Draft
1
13
feat: zero cost BaseIO changelog-compiler Compiler, runtime, and FFI changes-stage0 Contains stage0 changes, merge manually using rebase release-ci Enable all CI checks for a PR, like is done for releases toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#10625 opened Sep 30, 2025 by hargoniX • Draft
31
perf: build o.noexport from o.export instead of compiling from C code release-ci Enable all CI checks for a PR, like is done for releases toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#10623 opened Sep 30, 2025 by Rob23oba • Draft
3
fix: simp argument elaboration metacontext depth breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#10615 opened Sep 29, 2025 by kmill Loading…
1
2
ProTip! Follow long discussions with comments:>50.