Skip to content

Pull requests: leanprover/lean4

New pull request New
Clear current search query, filters, and sorts
252 Open 6,391 Closed
252 Open 6,391 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

fix: add groups around simpLemma and grindLemma syntax changelog-no Do not include this PR in the release changelog
#9157 opened Jul 2, 2025 by Rob23oba Loading…
fix: tighten IR typing rules for applications of closures changelog-compiler Compiler, runtime, and FFI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9154 opened Jul 2, 2025 by zwarich Loading…
6
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
2
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: typos in Std.Classes.Ord.Basic toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9145 opened Jul 1, 2025 by fgdorais Loading…
2
fix: module system: remove WellFounded-specific hacks 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
#9143 opened Jul 1, 2025 by nomeata Loading…
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
fix: undefined symbol without LEAN_USE_GMP backport releases/v4.22.0 changelog-other toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9106 opened Jun 30, 2025 by eric-wieser Loading…
6
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
#9100 opened Jun 30, 2025 by Kha Loading…
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 • Draft
6
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: replace some Subarray functions with generic slice functions breaks-manual This is not necessarily a blocker for merging, but there needs to be a plan. 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
#9017 opened Jun 26, 2025 by datokrat • Draft
8
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
fix: E-matching classes with HEq changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8999 opened Jun 25, 2025 by leodemoura • Draft
1
ProTip! no:milestone will show everything without a milestone.