Skip to content

Pull requests: leanprover/lean4

New pull request New
266 Open 6,553 Closed
266 Open 6,553 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

perf: simproc for grind normalizations and decls to unfold changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9202 opened Jul 5, 2025 by leodemoura Loading…
2
refactor: module-ize remainder of Std
#9195 opened Jul 4, 2025 by Kha • Draft
2
feat: Make Std.Do universe polymorphic
#9194 opened Jul 4, 2025 by sgraf812 • Draft
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
2
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…
12
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
6
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
minimization of build panic
#9126 opened Jul 1, 2025 by datokrat • Draft
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
refactor: module-ize Std.Time toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9100 opened Jun 30, 2025 by Kha Loading…
2
fix: add binrel% macros for notation in Init.Core 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
#9084 opened Jun 29, 2025 by plp127 Loading…
4
chore: add devcontainer 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
#9071 opened Jun 28, 2025 by tristan-f-r Loading…
2
feat: use letToHave system for computing dependent ldecls 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
#9070 opened Jun 28, 2025 by kmill Loading…
6
draft: minimization attempt for compiler error
#9056 opened Jun 28, 2025 by datokrat • Draft
feat: lake: pre-resolve module imports builds-mathlib CI has verified that Mathlib builds against this PR changelog-lake Lake toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9053 opened Jun 28, 2025 by tydeu Loading…
10
feat: improved go to definition 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
#9040 opened Jun 27, 2025 by mhuisi Loading…
1
refactor: Expose DeclNameGenerator idx toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9020 opened Jun 26, 2025 by lenianiva • Draft
3
refactor: remove InductiveVal.isReflexive 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
#9016 opened Jun 26, 2025 by cppio Loading…
10
fix: More stuck definitional equalities involving smart unfoldings (#8766) changelog-language Language features, tactics, and metaprograms
#9015 opened Jun 26, 2025 by sgraf812 Loading…
1
3
ProTip! no:milestone will show everything without a milestone.