- Notifications
You must be signed in to change notification settings - Fork 717
Pull requests: leanprover/lean4
Author
Label
Projects
Milestones
Reviews
Assignee
Sort
Pull requests list
perf: turn more bv_normalize rules into simprocs changelog-tactics User facing tactics
#11717 opened Dec 17, 2025 by hargoniX Loading…
perf: match compilation: pick out overlap assumption directly 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 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
refactor: remove IteratorCollect changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
feat: a grind configuration for use in match equation compilation changelog-language Language features and metaprograms
refactor: move error explanation text to the manual 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
#11688 opened Dec 15, 2025 by robsimmons • Draft
fix: add missing pp-spaces in A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
grind_pattern toolchain-available feat: lake: multi-version workspaces builds-mathlib CI has verified that Mathlib builds against this PR changelog-lake Lake 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
chore: add missing
.run and .mks in monad transformers #11647 opened Dec 13, 2025 by eric-wieser • Draft
perf: improve auto completion and fuzzy matching 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
refactor: grind AIG proofs into dust toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
feat: add We should not merge this until we have a successful Mathlib build changelog-tactics User facing tactics
grind +simp mode awaiting-mathlib #11601 opened Dec 11, 2025 by kim-em Loading…
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
feat: grind_pattern mod_eq_of_lt awaiting-review Waiting for someone to review the PR 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 changelog-library Library 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…
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…
fix: goto-definition for binrel% operators toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
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
feat: use approximate universe inverse when A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
sorry in inductive type toolchain-available 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 force-mathlib-ci 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
feat: Do not include this PR in the release changelog toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
termBeforeBy builtin parser changelog-no #11495 opened Dec 3, 2025 by JovanGerb Loading…
feat: add chunking support to 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
par and par' in Lean.Elab.Parallel builds-mathlib chore: CI: bump actions/checkout from 5 to 6 dependencies Pull requests that update a dependency file github_actions Pull requests that update GitHub Actions code toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11459 opened Dec 1, 2025 by dependabot bot Loading…
chore: CI: bump softprops/action-gh-release from 2.4.1 to 2.5.0 dependencies Pull requests that update a dependency file github_actions Pull requests that update GitHub Actions code toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11458 opened Dec 1, 2025 by dependabot bot Loading…
Previous Next
ProTip! What’s not been updated in a month: updated:<2025-11-17.