Skip to content

Pull requests: leanprover/lean4

New pull request New
333 Open 7,964 Closed
333 Open 7,964 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

feat: set_config for setting grind configuration options changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#10990 opened Oct 27, 2025 by leodemoura Loading…
2
doc: improve variable names and specify types in SMul doc toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#10989 opened Oct 27, 2025 by AxelBoldt Loading…
2
feat: eta-expand for oversaturating arguments while specializing (#10924) code-generator This issue is with the code generator
#10987 opened Oct 27, 2025 by sgraf812 • Draft
refactor: redefine String.replace
#10986 opened Oct 27, 2025 by TwoFX • Draft
fix: FunInd to beta-reduce abstracted proofs changelog-language Language features and metaprograms
#10981 opened Oct 27, 2025 by nomeata • Draft
1
1
feat: allow System.FilePath.walkDir to not follow symlinks toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#10973 opened Oct 26, 2025 by bibajz • Draft
1
4
chore: add grind test for future improvements to non-linear arithmetic.
#10970 opened Oct 26, 2025 by kim-em • Draft
chore: add deprecations for duplicated theorems awaiting-mathlib We should not merge this until we have a successful Mathlib build 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
#10967 opened Oct 26, 2025 by kim-em Loading…
4
feat: lake: require dependencies by semver range 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
#10959 opened Oct 25, 2025 by tydeu • Draft
2
feat: size builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#10952 opened Oct 25, 2025 by datokrat • Draft
2
feat: add union on ExtDTHashMap/ExtHashMap/ExtHashSet changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#10946 opened Oct 24, 2025 by wkrozowski • Draft
2
feat: Add Std.Trichotomous awaiting-author Waiting for PR author to address issues changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#10945 opened Oct 24, 2025 by linesthatinterlace Loading…
29
fix: Remove redundant instance requirement changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#10941 opened Oct 24, 2025 by linesthatinterlace Loading…
@datokrat
9
chore: add (failing) test for a grind panic toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#10921 opened Oct 23, 2025 by kim-em Loading…
2
feat: add union on DTreeMap/TreeMap/TreeSet changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#10896 opened Oct 22, 2025 by wkrozowski Loading…
2
chore: use Lake remote cache in CI builds-mathlib CI has verified that Mathlib builds against this PR changelog-no 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
#10880 opened Oct 21, 2025 by tydeu • Draft
2
feat: delab casesOn like match 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
#10876 opened Oct 21, 2025 by nomeata • Draft
4
feat: extrinsic finiteness proofs for loops on iterators builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#10863 opened Oct 21, 2025 by datokrat • Draft
8
fix: populate local instances during pretty printing 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
#10832 opened Oct 18, 2025 by thorimur • Draft
1
5
refactor: add MonadLift CoreM CommandElabM 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
#10829 opened Oct 17, 2025 by Kha • Draft
14
perf: sparse case splitting in match compilation breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#10823 opened Oct 17, 2025 by nomeata • Draft
2
perf: add missing std::moves to save refcounting toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#10816 opened Oct 17, 2025 by eric-wieser Loading…
6
fix: use assignment to implement optional<> move assignment changelog-none toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#10815 opened Oct 17, 2025 by eric-wieser Loading…
4
feat: revamp server logging 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
#10787 opened Oct 15, 2025 by mhuisi Loading…
2
feat: extrinsic finiteness proofs for toList, toListRev and toArray on iterators builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#10785 opened Oct 15, 2025 by datokrat Loading…
21
ProTip! Mix and match filters to narrow down what you’re looking for.