Skip to content

Pull requests: leanprover/lean4

New pull request New
654 Open 11,212 Closed
654 Open 11,212 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: basic reverse iterators for Range, Array, Vector toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15233 opened Sep 20, 2026 by Bubbler-4 Loading…
fix: lake: track cached ltar from partial unpack changelog-lake Lake toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15231 opened Sep 20, 2026 by tydeu Member Loading…
perf: non-quadratic floatLetIn toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15229 opened Sep 19, 2026 by hargoniX Member Loading…
4
fix: warn on deprecated fields in structure instances toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15225 opened Sep 19, 2026 by skwh54 • Draft
1
vibe-ported intblasting tests toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15224 opened Sep 18, 2026 by andres-erbsen • Draft
feat: delay elab of full file toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15222 opened Sep 18, 2026 by AugustDeer • Draft
1
feat: better handling of one-field-structure constructors and projections in induction/cases changelog-language Language features and metaprograms downstream Request a downstream-lean4 adaptation PR. toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15221 opened Sep 18, 2026 by datokrat Contributor • Draft
1
fix: prevent duplicate module initialization in C codegen awaiting-review Waiting for someone to review the PR toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15219 opened Sep 18, 2026 by iyassou • Draft
1
feat: extensible code formatter toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15218 opened Sep 18, 2026 by mhuisi Contributor • Draft
1
fix: reuse the instances of a non-exposed definition in inferInstanceAs changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15216 opened Sep 18, 2026 by gasparattila Loading…
1
1
fix: use pi_congr instead of forall_congr, deprecate the latter awaiting-review Waiting for someone to review the PR changelog-library Library downstream Request a downstream-lean4 adaptation PR. toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15215 opened Sep 18, 2026 by sgraf812 Contributor Loading…
1
4
test: robin's Level.isEquiv downstream Request a downstream-lean4 adaptation PR. toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15210 opened Sep 17, 2026 by arthur-adjedj Contributor • Draft
4
fix: include mutex in single-threaded thread.h awaiting-review Waiting for someone to review the PR changelog-compiler Compiler, runtime, and FFI
#15209 opened Sep 17, 2026 by Chessing234 Loading…
1
2
fix: error instead of panic on excess syntax match patterns awaiting-review Waiting for someone to review the PR changelog-language Language features and metaprograms
#15208 opened Sep 17, 2026 by Chessing234 Loading…
1
2
fix: preserve outer messages around #guard_msgs awaiting-review Waiting for someone to review the PR changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15207 opened Sep 17, 2026 by Chessing234 Loading…
1
2
fix: preserve binder names in lambdaMetaTelescope awaiting-review Waiting for someone to review the PR changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15206 opened Sep 17, 2026 by Chessing234 Loading…
1
2
fix: bound JSON number exponents below Nat.pow panic awaiting-review Waiting for someone to review the PR changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15205 opened Sep 17, 2026 by Chessing234 Loading…
1
2
fix: error on ← modifier for simprocs and simp extensions awaiting-review Waiting for someone to review the PR changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15204 opened Sep 17, 2026 by Chessing234 Loading…
1
2
fix: require panic prefix in #guard_panic awaiting-review Waiting for someone to review the PR changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15202 opened Sep 17, 2026 by Chessing234 Loading…
1
2
test: lean4Lean's Level.isEquiv downstream Request a downstream-lean4 adaptation PR. toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15198 opened Sep 17, 2026 by arthur-adjedj Contributor • Draft
5
fix: do not evaluate Nat left shifts the runtime cannot perform toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15194 opened Sep 17, 2026 by gersh • Draft
1
fix: cancellation in ContextAsync and wakeups in Notify, Channel and Broadcast changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15192 opened Sep 17, 2026 by algebraic-dev Member Loading…
@algebraic-dev
fix: make timers and signals safe against re-entrant continuations and lost signals changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15191 opened Sep 17, 2026 by algebraic-dev Member Loading…
@algebraic-dev
refactor: use Sym.Arith classification in the grind ring solver changelog-tactics User facing tactics
#15190 opened Sep 17, 2026 by leodemoura Member Loading…
fix: preserve restored Lake archives for output tracking changelog-lake Lake toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15189 opened Sep 16, 2026 by kim-em Collaborator • Draft
1
ProTip! Adding no:label will show everything without a label.