Skip to content

Pull requests: leanprover/lean4

New pull request New
291 Open 6,863 Closed
291 Open 6,863 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 idxOf Verification API
#9613 opened Jul 29, 2025 by DavidJWebb • Draft
feat: note potential discrepancies in deprecation warning 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
#9606 opened Jul 29, 2025 by jrr6 • Draft
1
2
fix: lake: thin archives for Windows bootstrap only changelog-lake Lake toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9604 opened Jul 28, 2025 by tydeu Loading…
1
perf: getStuckMVar? changelog-no Do not include this PR in the release changelog
#9603 opened Jul 28, 2025 by leodemoura Loading…
chore: don't check type of erased arguments in FixedParams analysis toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9602 opened Jul 28, 2025 by zwarich Loading…
4
feat: add support for lazy hints via lazy code action sets breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan 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
#9601 opened Jul 28, 2025 by jrr6 • Draft
2
feat: add useful functions in Parsec and add error variant changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9599 opened Jul 28, 2025 by algebraic-dev Loading…
@algebraic-dev
2
perf: optimize Name.toString changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9594 opened Jul 28, 2025 by hargoniX Loading…
9
chore: simplify docstring for propext changelog-doc Documentation documentation Documentation improvement toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9593 opened Jul 28, 2025 by david-christiansen • Queued
2
feat: update structure/inductive 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
#9592 opened Jul 28, 2025 by jrr6 Loading…
2
perf: clarify and granularize access to async env ext state 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
#9587 opened Jul 28, 2025 by Kha • Draft
8
feat: (experimental) changes to transparency escalation 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
#9585 opened Jul 28, 2025 by kim-em • Draft
2
feat: improved instance synth order
#9582 opened Jul 27, 2025 by JovanGerb • Draft
perf: optimize fuzzyMatching toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9563 opened Jul 26, 2025 by hargoniX • Draft
10
fix: background function and forIn changelog-library Library
#9560 opened Jul 26, 2025 by algebraic-dev Loading…
@algebraic-dev
1
fix: lake: use server header for workspace modules changelog-lake Lake
#9559 opened Jul 26, 2025 by tydeu • Draft
8
feat: make #check log stuck instance synthesis changelog-language Language features, tactics, and metaprograms
#9554 opened Jul 25, 2025 by kmill Loading…
feat: add BEq instance for ByteArray that uses memcmp changelog-library Library
#9549 opened Jul 25, 2025 by algebraic-dev Loading…
@algebraic-dev
4
refactor: minimize Lean.Meta.Diagnostics imports
#9546 opened Jul 25, 2025 by Kha Loading…
refactor: minimize Lean.Meta.Tactic.TryThis imports
#9539 opened Jul 25, 2025 by Kha Loading…
2
chore: [match_pattern] should enforce [expose] toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9534 opened Jul 25, 2025 by Kha Loading…
2
feat: suppress deprecation warnings inside deprecated declarations toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9533 opened Jul 25, 2025 by jkpjkpjkp Loading…
1
2
feat: elaboration with empty tactic sequences changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9524 opened Jul 25, 2025 by kmill • Draft
2
feat: add List.mem_finRange toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9515 opened Jul 24, 2025 by fgdorais Loading…
2
fix: Make mvcgen mintro let/have bindings (#9474) changelog-language Language features, tactics, and metaprograms
#9507 opened Jul 24, 2025 by sgraf812 Loading…
1
ProTip! Exclude everything labeled bug with -label:bug.