Skip to content

Pull requests: leanprover/lean4

New pull request New
555 Open 10,207 Closed
555 Open 10,207 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: lake: conditional cache overwrites changelog-lake Lake mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14036 opened Jun 12, 2026 by tydeu Member • Draft
1
perf: outline heartbeat inc toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14035 opened Jun 12, 2026 by hargoniX Contributor • Draft
8
feat: add Triple.post_imp_elim and Triple.rotate_pre changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14034 opened Jun 12, 2026 by sgraf812 Contributor Loading…
2
perf: worst case n log n complexity for Array.qsort toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14033 opened Jun 12, 2026 by johanphenkel-cmd • Draft
1
@TwoFX
4
perf: parallel pre-read of import regions with --setup toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14032 opened Jun 12, 2026 by Kha Member Loading…
6
doc: fix typo in Format.bracketFill documentation toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14018 opened Jun 11, 2026 by ia0 Loading…
2
feat: port the mvcgen' tactic to the new Std.Internal.Do meta theory changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14015 opened Jun 11, 2026 by sgraf812 Contributor Loading…
6
doc: fix typo in Format.nest example toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14013 opened Jun 11, 2026 by ia0 Loading…
3
perf: avoid expensive instance re-synthesis in cbv changelog-language Language features and metaprograms
#14009 opened Jun 11, 2026 by wkrozowski Contributor • Draft
2
perf: optimizations for PHashMap
#14007 opened Jun 11, 2026 by hargoniX Contributor • Draft
doc(lake): expand require ... with <opts> documentation and -K propagation guidance
#14006 opened Jun 11, 2026 by kim-em Collaborator Loading…
fix: lake: skip artifacts already present when staging or unstaging
#14002 opened Jun 11, 2026 by marcelolynch Contributor Loading…
1
feat: new Path library for Std changelog-library Library
#13998 opened Jun 10, 2026 by algebraic-dev Member Loading…
@algebraic-dev
feat: make Bool.xor a standalone definition
#13995 opened Jun 10, 2026 by linesthatinterlace Contributor • Draft
1
feat(lake): content-stable module archives in Lake's artifact cache toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13992 opened Jun 10, 2026 by marcelolynch Contributor • Draft
2
4
fix: mkBindUnlessPure should call the continuation only once builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features and metaprograms mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13985 opened Jun 9, 2026 by Rob23oba Contributor Loading…
1
2
[test] faster isDefEqApp builds-mathlib CI has verified that Mathlib builds against this PR mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13979 opened Jun 9, 2026 by datokrat Contributor • Draft
6
feat: redesign mvcgen' for a new meta theory changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13978 opened Jun 9, 2026 by volodeyka Contributor • Draft
2
feat: generalize Sym.Pattern construction over binder telescopes toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13972 opened Jun 8, 2026 by sgraf812 Contributor • Draft
4
feat: detect and special case ITE/XORs when lowering AIG to CNF changelog-tactics User facing tactics 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
#13968 opened Jun 8, 2026 by georgerennie Contributor Loading…
5
doc: fix incorrect examples of K-like reduction in RecursorVal docstring builds-mathlib CI has verified that Mathlib builds against this PR mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13967 opened Jun 7, 2026 by berberman Contributor Loading…
4
fix: preserve revert argument order changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13964 opened Jun 7, 2026 by asvitha2000 Loading…
1
3
feat: bound kernel recursion by maxRecDepth builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features and metaprograms mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13956 opened Jun 4, 2026 by Kha Member Loading…
9
feat(lake): wrapped exec toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13948 opened Jun 3, 2026 by marcelolynch Contributor • Draft
15
fix: indent #guard_msgs code action to match command indentation toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13947 opened Jun 3, 2026 by rdavison Loading…
2
ProTip! no:milestone will show everything without a milestone.