Skip to content

Pull requests: leanprover/lean4

New pull request New
256 Open 5,743 Closed
256 Open 5,743 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
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

feat: optimize lean_nat_shiftr for scalars changelog-compiler Compiler, runtime, and FFI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8268 opened May 8, 2025 by zwarich Loading…
1
feat: guard_msgs to treat trace messages separate 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
#8267 opened May 8, 2025 by nomeata • Queued
1
6
feat: improve infer binder type failure message and range 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
#8263 opened May 8, 2025 by Kha Loading…
fix: improve type-as-hole error message 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
#8262 opened May 8, 2025 by leodemoura Loading…
3
fix: invalid dotted identifier notation error for sort changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8260 opened May 8, 2025 by tydeu Loading…
2
fix: invalid field notation error for mvar changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8259 opened May 8, 2025 by tydeu Loading…
1
feat: add toInt_smod
#8253 opened May 7, 2025 by luisacicolini • Draft
fix: nested try-catch parsing 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
#8252 opened May 6, 2025 by Rob23oba Loading…
1
1
feat: add @[grind] annotations for HashMap/TreeMap 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
#8246 opened May 6, 2025 by kim-em • Draft
1
fix: deduplicate elaboration of constant argument to rw 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
#8232 opened May 5, 2025 by JovanGerb Loading…
2
feat: guard against synthetic sorry misuse backport releases/v4.20.0 changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8230 opened May 5, 2025 by Kha • Draft
2
chore: link against system glibc
#8229 opened May 5, 2025 by Kha • Draft
fix: make "invalid use of 'partial' error" more robust changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8227 opened May 5, 2025 by kim-em Loading…
2
feat: do not export def bodies by default changelog-language Language features, tactics, and metaprograms
#8221 opened May 4, 2025 by Kha • Draft
4
fix: rfl theorem tracking in the module system 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
#8215 opened May 3, 2025 by Kha Loading…
10
fix: aborting elaboration should not lead to empty #print axioms builds-mathlib CI has verified that Mathlib builds against this PR changelog-other toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8214 opened May 3, 2025 by Kha Loading…
1
feat: equivalence of tree maps changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8210 opened May 2, 2025 by Rob23oba • Draft
1
feat: BitVec.neg_ofNat_eq_ofInt_neg toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8206 opened May 2, 2025 by bollu • Draft
1
feat: simplify T-division into E-division when numerator is positive. 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
#8205 opened May 2, 2025 by bollu • Draft
2
feat: characterize when T-division equals zero 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
#8204 opened May 2, 2025 by bollu • Draft
2
feat: Bitvector trichotomy lemmas 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
#8203 opened May 2, 2025 by bollu • Draft
4
fix: broken unknown identifier code actions 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
#8180 opened Apr 30, 2025 by mhuisi Loading…
1
feat: BitVec.msb_sdiv toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8178 opened Apr 30, 2025 by bollu • Draft
13
doc: add documentation for builtin attributes 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
#8173 opened Apr 30, 2025 by Rob23oba • Draft
12
fix: correct whitespace in omit/include changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8169 opened Apr 30, 2025 by eric-wieser Loading…
2
ProTip! What’s not been updated in a month: updated:<2025-04-08.