Skip to content

Pull requests: leanprover/lean4

New pull request New
171 Open 3,890 Closed
171 Open 3,890 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

refactor: name the default SizeOf instance
#5981 opened Nov 6, 2024 by nomeata Loading…
refactor: use Json.null to represent Name.anonymous 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
#5980 opened Nov 6, 2024 by tydeu Loading…
2
feat: simp -underLambda 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
#5977 opened Nov 6, 2024 by nomeata • Draft
chore: new PR changelog template 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
#5976 opened Nov 6, 2024 by Kha Loading…
3
fix: out of scope let-variable can appear in fun binder type of metav… 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
#5948 opened Nov 5, 2024 by JovanGerb • Draft
1
feat: message kinds 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
#5945 opened Nov 4, 2024 by tydeu Loading…
6
fix: add cmake COPY_CADICAL option to allow turning off install copy toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#5931 opened Nov 3, 2024 by juhp Loading…
1
7
feat: float_match simproc and conv tactic 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
#5923 opened Nov 1, 2024 by nomeata Loading…
2
feat: all direct parents of classes create projections 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
#5920 opened Nov 1, 2024 by kmill Loading…
1
1
fix: unset trailing for simpa? "try this" suggestion 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
#5907 opened Oct 31, 2024 by kmill Loading…
1
1
feat: Upstream derive handler for ToExpr from Mathlib
#5906 opened Oct 31, 2024 by alexkeizer • Draft
3
feat: verify keys method on HashMaps toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#5866 opened Oct 28, 2024 by monsterkrampe Loading…
@TwoFX
4
feat: elaborate theorem bodies in parallel
#5864 opened Oct 28, 2024 by Kha • Draft
6
feat: prop instance yields theorems awaiting-review Waiting for someone to review the PR 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
#5856 opened Oct 26, 2024 by kmill Loading…
1
2
feat: structural recursion: support more nested matches
#5849 opened Oct 26, 2024 by nomeata • Draft
feat: stronger proof strategy for partial inhabitation awaiting-review Waiting for someone to review the PR 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
#5847 opened Oct 26, 2024 by kmill Loading…
1
fix: Only consider salient bytes in sharecommon eq, hash toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#5840 opened Oct 25, 2024 by tkoeppe Loading…
1
5
feat: rsimp_decide etc 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
#5839 opened Oct 25, 2024 by nomeata • Draft
1
fix: don't issue atomic id completions when there is a dangling dot toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#5837 opened Oct 25, 2024 by mhuisi • Draft
1
feat: structure auto-completion & partial InfoTrees toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#5835 opened Oct 25, 2024 by mhuisi Loading…
1
15
fix: make prefix ! require that there be no whitespace after it 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
#5826 opened Oct 23, 2024 by kmill • Draft
1
fix: reduce precedence of prefix ! to 'lead' toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#5824 opened Oct 23, 2024 by kmill • Draft
1
feat: Pass argv[0] to main P-high We will work on this issue 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
#5820 opened Oct 23, 2024 by eric-wieser Loading…
1
24
feat: BitVec.toInt_abs awaiting-author Waiting for PR author to address issues toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#5787 opened Oct 21, 2024 by bollu • Draft
22
feat: labeled and unique sorries toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#5757 opened Oct 17, 2024 by kmill Loading…
1
9
ProTip! What’s not been updated in a month: updated:<2024-10-06.