Content-Length: 361331 | pFad | http://github.com/leanprover/lean4/pulls

7B Pull requests · leanprover/lean4 · GitHub
Skip to content

Pull requests: leanprover/lean4

New pull request New
272 Open 6,631 Closed
272 Open 6,631 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

chore: minor perf improvement changelog-no Do not include this PR in the release changelog
#9296 opened Jul 10, 2025 by leodemoura • Queued
perf: minor performance improvement to reduceCtorEq simproc changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9295 opened Jul 10, 2025 by leodemoura Loading…
3
perf: don't use discr-based opts for ctors with no fields changelog-compiler Compiler, runtime, and FFI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9288 opened Jul 9, 2025 by zwarich • Draft
5
fix: reorder "application type mismatch" message 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
#9287 opened Jul 9, 2025 by jrr6 Loading…
4
fix: remove BEq from (Array|Vector).(any|all)_push changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9285 opened Jul 9, 2025 by Tasiro Loading…
@TwoFX
2
refactor: remove now-unused type_context constructors toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9282 opened Jul 9, 2025 by zwarich Loading…
2
refactor: remove Lean.RBMap
#9260 opened Jul 8, 2025 by hargoniX • Draft
6
feat: add signal handling support using libuv changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9258 opened Jul 8, 2025 by algebraic-dev Loading…
@algebraic-dev
7
draft: improve order-related typeclass hierarchy
#9248 opened Jul 8, 2025 by datokrat • Draft
chore: reintroduce Subarray.foldl on top of Slice.foldl toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9234 opened Jul 7, 2025 by datokrat • Draft
2
fix: mark irrelevant params as erased in mono type signatures changelog-compiler Compiler, runtime, and FFI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9226 opened Jul 7, 2025 by zwarich Loading…
6
fix: erase constructor params in toMono changelog-compiler Compiler, runtime, and FFI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9222 opened Jul 6, 2025 by zwarich • Draft
9
chore: mark Nat.cast and Int.cast with pp_nodot toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9208 opened Jul 5, 2025 by plp127 Loading…
5
refactor: module-ize remainder of Std toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9195 opened Jul 4, 2025 by Kha • Draft
4
fix: unfold abstracted proofs before processing recursion 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
#9191 opened Jul 4, 2025 by nomeata • Draft
1
3
doc: correct the Option.getD docString example toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9190 opened Jul 4, 2025 by Mal-Pat Loading…
1
2
refactor: module-ize Std.Internal.Async
#9188 opened Jul 4, 2025 by Kha Loading…
chore: fix spelling errors 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
#9175 opened Jul 3, 2025 by Rob23oba Loading…
21
feat: Add prohibit unsafe flag toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9148 opened Jul 2, 2025 by lenianiva • Draft
8
feat: improve performance of usedOnly and usedLetOnly for MetavarContext.mkBinding builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features, tactics, and metaprograms force-mathlib-ci toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9147 opened Jul 2, 2025 by kmill • Draft
2
fix: use let rec for Fin.reverseInduction changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9142 opened Jul 1, 2025 by kckennylau Loading…
1
2
chore: demote a panic to an exception in saveModuleData changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9127 opened Jul 1, 2025 by eric-wieser Loading…
3
perf: kernel defeq breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-other toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9122 opened Jul 1, 2025 by leodemoura Loading…
3
fix: simp? output order changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9117 opened Jul 1, 2025 by Rob23oba Loading…
1
2
chore: lake: re-enable tests in CI changelog-no Do not include this PR in the release changelog
#9104 opened Jun 30, 2025 by tydeu • Draft
ProTip! Find all pull requests that aren't related to any open issues with -linked:issue.








ApplySandwichStrip

pFad - (p)hone/(F)rame/(a)nonymizer/(d)eclutterfier!      Saves Data!


--- a PPN by Garber Painting Akron. With Image Size Reduction included!

Fetched URL: http://github.com/leanprover/lean4/pulls

Alternative Proxies:

Alternative Proxy

pFad Proxy

pFad v3 Proxy

pFad v4 Proxy