Skip to content

Pull requests: leanprover/lean4

New pull request New
177 Open 4,107 Closed
177 Open 4,107 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

fix: have Lean.Meta.isConstructorApp'? be aware of n + k Nat offsets changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6270 opened Dec 1, 2024 by kmill Loading…
1
feat: warnings when declarations and export aliases conflict awaiting-review Waiting for someone to review the PR 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
#6269 opened Dec 1, 2024 by kmill Loading…
1
1
feat: dotParam widget to control dot notation changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6267 opened Nov 30, 2024 by kmill • Draft
2
1
chore: remove accidentally added file changelog-no Do not include this PR in the release changelog
#6262 opened Nov 29, 2024 by hargoniX Loading…
experiment: induction principles for non-recursive functions 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
#6261 opened Nov 29, 2024 by nomeata • Draft
1
debug: disable ofReduceBool to catch actual kernel errors 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
#6248 opened Nov 28, 2024 by hargoniX • Draft
1
feat: reverse HashMap.toList, so it agrees with HashMap.toArray 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
#6244 opened Nov 28, 2024 by kim-em Loading…
2
feat: remove runtime bounds checks and partial from qsort changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6241 opened Nov 28, 2024 by kim-em Loading…
3
feat: BitVec.toFin/ToInt BitVec.ushiftRight awaiting-review Waiting for someone to review the PR 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
#6238 opened Nov 27, 2024 by bollu Loading…
11
feat: HashMap.toList_map_fst changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6232 opened Nov 27, 2024 by kim-em • Draft
2
feat: add Timer and a global event loop in a separate thread using LibUV toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6219 opened Nov 26, 2024 by algebraic-dev • Draft
28
chore: upstream nolint attribute
#6215 opened Nov 25, 2024 by jcommelin • Draft
refactor: move registration of namespaces on kernel add into elaborator
#6214 opened Nov 25, 2024 by Kha Loading…
feat: verify insertMany method for adding lists to HashMaps toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6211 opened Nov 25, 2024 by monsterkrampe • Draft
@TwoFX
28
chore: Elab.async benchmarking 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
#6210 opened Nov 25, 2024 by Kha • Draft
3
feat: _ separators in numeric literals awaiting-review Waiting for someone to review the PR 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
#6204 opened Nov 25, 2024 by kmill Loading…
1
1
fix: missing (type := true) in reader monad example 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
#6196 opened Nov 24, 2024 by jsr-p Loading…
1
feat: more UInt bitwise theorems 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
#6188 opened Nov 23, 2024 by tydeu Loading…
1
feat: BitVec.[toInt|toFin]_concat and Bool.toInt awaiting-review Waiting for someone to review the PR 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
#6182 opened Nov 23, 2024 by tobiasgrosser Loading…
12
feat: add BitVec.[toNat|toInt|toFin|getLsbD|getMsbD|getElem|msb]_fill 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
#6177 opened Nov 22, 2024 by tobiasgrosser Loading…
4
feat: lake: build without leanc builds-mathlib CI has verified that Mathlib builds against this PR changelog-lake Lake release-ci Enable all CI checks for a PR, like is done for releases toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6176 opened Nov 22, 2024 by tydeu Loading…
1
fix: propagate Simp.Config when reducing terms and checking definitional equality in simp 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
#6123 opened Nov 19, 2024 by leodemoura Loading…
1
4
feat: attribute delaborators breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-pp Pretty printing toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6115 opened Nov 18, 2024 by digama0 • Draft
1
5
feat: allow limiting the number of binders in delabConstWithSignature toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6092 opened Nov 15, 2024 by eric-wieser • Draft
3
doc: MkBinding.abstractRange doesn't do anything with types of free variables P-medium We may work on this issue if we find the time toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6089 opened Nov 15, 2024 by JovanGerb Loading…
1
ProTip! Type g i on any issue or pull request to go back to the issue listing page.