Skip to content

Pull requests: leanprover/lean4

New pull request New
510 Open 9,799 Closed
510 Open 9,799 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: add missing noexcepts
#13370 opened Apr 10, 2026 by eric-wieser Contributor Loading…
feat: add type-correctness note to rewrite tactic error messages
#13368 opened Apr 10, 2026 by Kha Member • Draft
1
fix: prevent a hang in acLt 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
#13367 opened Apr 10, 2026 by eric-wieser Contributor Loading…
6
feat: use right-associativity in Level.max normalization breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan 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
#13366 opened Apr 10, 2026 by kmill Collaborator • Draft
1
3
refactor: stop bumping transparency to .instances in whnfMatcher 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
#13363 opened Apr 10, 2026 by nomeata Collaborator • Draft
2
test toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13362 opened Apr 10, 2026 by hargoniX Contributor • Draft
4
fix: use fresh universe metavariables in wrapInstance 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
#13361 opened Apr 10, 2026 by JovanGerb Contributor Loading…
3
fix: end_local_scope does not work with compound namespace names changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13360 opened Apr 10, 2026 by wkrozowski Contributor Loading…
1
2
feat: add linter.redundantExpose for redundant @[expose]/@[no_expose] attributes breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan 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
#13359 opened Apr 10, 2026 by Kha Member • Draft
2
proof of concept: simp lemmas spawing subgoals toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13358 opened Apr 10, 2026 by datokrat Contributor • Draft
2
feat: upstream environment linters to core lean changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13356 opened Apr 10, 2026 by wkrozowski Contributor Loading…
2
fix: decLevel? should normalize breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan 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
#13352 opened Apr 9, 2026 by kmill Collaborator • Draft
7
fix: fresh result type in ControlLifter.lift for monad resolution changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13349 opened Apr 9, 2026 by sgraf812 Contributor Loading…
2
fix: tactic completion in empty by blocks 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
#13348 opened Apr 9, 2026 by mhuisi Contributor Loading…
2
fix: keep wrapInstance mvar-free builds-mathlib CI has verified that Mathlib builds against this PR changelog-no Do not include this PR in the release changelog 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
#13346 opened Apr 9, 2026 by Kha Member Loading…
6
fix: backward defeq types compat fixes for bv_decide breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan 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
#13345 opened Apr 9, 2026 by hargoniX Contributor • Draft
3
fix: instantiate and normalize level metavariables in getLevel 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
#13343 opened Apr 9, 2026 by sgraf812 Contributor Loading…
12
fix: respect transparency breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan 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
#13342 opened Apr 9, 2026 by datokrat Contributor • Draft
6
chore: cache-get Make target toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13341 opened Apr 9, 2026 by Kha Member Loading…
3
refactor: grind ring module changelog-tactics User facing tactics
#13339 opened Apr 9, 2026 by leodemoura Member • Draft
perf: faster fast path for expr defeq toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13338 opened Apr 8, 2026 by hargoniX Contributor • Draft
4
fix: add term info for for loop in new do elaborator 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
#13337 opened Apr 8, 2026 by Rob23oba Contributor Loading…
1
2
doc: clarify that BitVec intMin/intMax refer to two's complement interpretation toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13336 opened Apr 8, 2026 by plimkilde Loading…
2
feat: add a check for impossible arguments in instance definitions awaiting-mathlib We should not merge this until we have a successful Mathlib build changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13333 opened Apr 8, 2026 by wkrozowski Contributor Loading…
4
fix: make local elab use privately imported meta defs breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan 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
#13331 opened Apr 8, 2026 by Komyyy Contributor • Draft
1
6
ProTip! Adding no:label will show everything without a label.