Skip to content

Pull requests: leanprover/lean4

New pull request New
366 Open 8,465 Closed
366 Open 8,465 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: realization of private def should run in private scope
#11618 opened Dec 11, 2025 by Kha Loading…
1
perf: avoid kernel env block in realizeConst
#11617 opened Dec 11, 2025 by Kha Loading…
1
perf: more environment blocking avoidance
#11616 opened Dec 11, 2025 by Kha Loading…
1
refactor: grind AIG proofs into dust
#11614 opened Dec 11, 2025 by hargoniX • Draft
chore: use backticks for sorry in diagnostic messages
#11608 opened Dec 11, 2025 by alok Loading…
3 tasks done
fix: proper error messages for Std.Do tactic invokations without arguments (#11509) changelog-language Language features and metaprograms
#11607 opened Dec 11, 2025 by sgraf812 Loading…
1
perf: avoid blocking on proof elaboration in Environment.hasUnsafe builds-manual CI has verified that the Lean Language Reference builds against this PR 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
#11606 opened Dec 11, 2025 by Kha • Queued
6
feat: add grind +simp mode awaiting-mathlib We should not merge this until we have a successful Mathlib build changelog-tactics User facing tactics
#11601 opened Dec 11, 2025 by kim-em Loading…
feat: add lemmas about EStateM.run changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11600 opened Dec 11, 2025 by eric-wieser Loading…
4
feat: @[suggest_for ℤ] and @[suggest_for ℚ] annotations changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11596 opened Dec 11, 2025 by kim-em Loading…
3
feat: suggestions for some size/count/length confusions changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11588 opened Dec 10, 2025 by robsimmons • Draft
3
feat: do not have meta imply partial awaiting-mathlib We should not merge this until we have a successful Mathlib build 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 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
#11587 opened Dec 10, 2025 by Kha Loading…
6
feat: grind_pattern mod_eq_of_lt awaiting-author Waiting for PR author to address issues builds-manual CI has verified that the Lean Language Reference builds against this PR 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
#11584 opened Dec 10, 2025 by pirapira Loading…
7
doc: adds missing docstrings related to iterators and ranges changelog-doc Documentation toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11563 opened Dec 9, 2025 by david-christiansen Loading…
2
fix: goto-definition for binrel% operators toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11558 opened Dec 9, 2025 by alok • Draft
2
refactor: make simpH proof-producing 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
#11553 opened Dec 8, 2025 by nomeata • Draft
2
fix: add table variant for require.git field in lakefile.toml schema builds-mathlib CI has verified that Mathlib builds against this PR changelog-server Language server, widgets, and IDE extensions 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
#11536 opened Dec 7, 2025 by maxwell3025 Loading…
1
13
chore: update projection/field access wording toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11533 opened Dec 6, 2025 by robsimmons • Draft
2
feat: MonadAttach changelog-library Library
#11532 opened Dec 6, 2025 by datokrat • Draft
4
feat: add a lemma relating minKey? and min? for DTreeMap changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11528 opened Dec 5, 2025 by wkrozowski Loading…
6
feat: add decidable equality to DTreeMap/TreeMap/TreeSet and their extensional variants changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11527 opened Dec 5, 2025 by wkrozowski Loading…
2
feat: use approximate universe inverse when sorry in inductive type toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11524 opened Dec 5, 2025 by kmill • Draft
3
fix: more robust match equation generation breaks-manual This is not necessarily a blocker for merging, but there needs to be a plan. 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
#11512 opened Dec 4, 2025 by nomeata • Draft
8
feat: lint coercions that are deprecated or banned in core builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11511 opened Dec 4, 2025 by datokrat Loading…
8
feat: introduce Context type for cancellation with context propagation changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11499 opened Dec 3, 2025 by algebraic-dev Loading…
@algebraic-dev
18
ProTip! Type g i on any issue or pull request to go back to the issue listing page.