Skip to content

Pull requests: leanprover/lean4

New pull request New
277 Open 6,796 Closed
277 Open 6,796 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: add List.mem_finRange
#9515 opened Jul 24, 2025 by fgdorais Loading…
fix: expose LCNF of private inline decl referenced by implemented_by
#9514 opened Jul 24, 2025 by Kha Loading…
chore: minimize benchmark imports so we don't spend a majority in importing
#9513 opened Jul 24, 2025 by Kha • Queued
fix: Make mvcgen mintro let/have bindings (#9474) changelog-language Language features, tactics, and metaprograms
#9507 opened Jul 24, 2025 by sgraf812 Loading…
1
feat: improve set_option error messages 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
#9496 opened Jul 23, 2025 by jrr6 Loading…
2
refactor: update and consolidate attribute-related error messages 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
#9495 opened Jul 23, 2025 by jrr6 • Draft
2
fix: avoid RPC errors in nonexistent identifier hovers changelog-pp Pretty printing toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9494 opened Jul 23, 2025 by jrr6 Loading…
2
fix: let simp apply autogenerated congruence theorems 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
#9493 opened Jul 23, 2025 by kmill • Draft
1
2
feat: have structure instances try synthesizing pending mvars before postponing 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
#9490 opened Jul 23, 2025 by kmill • Draft
4
feat: popCount for bv_decide (simple circuit)
#9469 opened Jul 22, 2025 by luisacicolini • Draft
feat: allow short config syntax (+opt / -opt) for several parsers changelog-language Language features, tactics, and metaprograms
#9437 opened Jul 19, 2025 by Rob23oba Loading…
3
feat: integrate OrderData with BEq and Ord changelog-library Library
#9430 opened Jul 18, 2025 by datokrat • Draft
feat: add popCount using Kernighan's algorithm to the bitblaster
#9416 opened Jul 17, 2025 by luisacicolini • Draft
chore: CI: reactivate Lake cache toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9401 opened Jul 16, 2025 by Kha • Draft
2
feat: high-level order structures breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9379 opened Jul 15, 2025 by datokrat • Draft
2
feat: generate (co)induction proof principles for mutually (co)inductive predicates changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9358 opened Jul 14, 2025 by wkrozowski Loading…
5
chore: hypothetical PR for grove changelog-no Do not include this PR in the release changelog grove The standard library changes in this PR should be analyzed using Grove. toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9355 opened Jul 14, 2025 by TwoFX • Draft
3
feat: use synthetic metavariables for autoparams (experiment) 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
#9346 opened Jul 13, 2025 by kmill • Draft
2
chore: rely on xType field rather than recomputing it toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9345 opened Jul 13, 2025 by zwarich Loading…
11
refactor: module-ize Lean
#9330 opened Jul 12, 2025 by Kha • Draft
11
perf: remove grind blockers
#9328 opened Jul 12, 2025 by Kha Loading…
6
perf: remove obsolete old codegen workaround 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
#9311 opened Jul 11, 2025 by Kha Loading…
6
chore: fix acNf bug in bv_decide by switching over to grind
#9309 opened Jul 11, 2025 by bollu • Draft
2
feat: make Option.decidableEqNone coherent with Option.instDecidableEq awaiting-author Waiting for PR author to address issues breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-library Library P-high We will work on this issue toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9302 opened Jul 10, 2025 by plp127 Loading…
@TwoFX
13
perf: deduplicate core computation inside mkCongrSimpForConst? 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 force-mathlib-ci toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9300 opened Jul 10, 2025 by Kha • Draft
9
ProTip! Follow long discussions with comments:>50.