8000 Pull requests · leanprover/lean4 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Pull requests: leanprover/lean4

New pull request New
278 Open 6,360 Closed
278 Open 6,360 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

chore: initial Grove setup 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
#8997 opened Jun 25, 2025 by TwoFX • Draft
1
feat: Hoare logic for monadic programs and verification condition generation awaiting-mathlib We should not merge this until we have a successful Mathlib build changelog-language Language features, tactics, and metaprograms changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8995 opened Jun 25, 2025 by sgraf812 • Draft
feat: generalize withCtor functions to eliminate to Sort toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8994 opened Jun 25, 2025 by nomeata • Draft
2
fix: do not assign mvars when validating unification hint conclusion changelog-language Language features, tactics, and metaprograms
#8988 opened Jun 25, 2025 by cppio • Draft
1
1
feat: improve projection and field-notation errors toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8986 opened Jun 25, 2025 by jrr6 • Draft
1
chore: try to expose more of Lean.Grind.CommRing
#8985 opened Jun 25, 2025 by kim-em Loading…
1
chore: use note and hint' for message addenda changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8980 opened Jun 24, 2025 by jrr6 Loading…
5
fix: make hasLocalInst ignore instance params of erased type changelog-compiler Compiler, runtime, and FFI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8979 opened Jun 24, 2025 by zwarich • Draft
10
feat: introduce MonadLiftT Id m changelog-library Library
#8977 opened Jun 24, 2025 by datokrat Loading…
feat: add BitVec.msb_(smod, srem) changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8974 opened Jun 24, 2025 by luisacicolini • Queued
24
feat: optimized simp routine for let telescopes changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8968 opened Jun 24, 2025 by kmill Loading…
2
feat: add BitVec.toFin_(sdiv, smod, srem) and BitVec.toNat_srem changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8950 opened Jun 23, 2025 by luisacicolini • Draft
20
feat: introduce slices changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8947 opened Jun 23, 2025 by datokrat • Draft
1
fix: remove the IR elim_dead_branches pass changelog-compiler Compiler, runtime, and FFI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8932 opened Jun 23, 2025 by zwarich • Draft
10
feat: Upstream MPL.SPred.* from mpl awaiting-mathlib We should not merge this until we have a successful Mathlib build breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8928 opened Jun 22, 2025 by sgraf812 Loading…
10
feat: lake: local artifact cache builds-mathlib CI has verified that Mathlib builds against this PR changelog-lake Lake toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8922 opened Jun 22, 2025 by tydeu • Draft
3
fix: use an unreachable default for cases with > 2 alts changelog-compiler Compiler, runtime, and FFI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8917 opened Jun 21, 2025 by zwarich • Draft
1
4
perf: use MVarId.assign instead of isDefEq in type class search 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
#8915 opened Jun 21, 2025 by JovanGerb • Draft
1
feat: improve error message when passing local hypotheses to grind 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
#8891 opened Jun 20, 2025 by marcusrossel • Draft
3
fix: match discriminant congruence in simp 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
#8884 opened Jun 19, 2025 by Rob23oba Loading…
1
35
perf: better isDefEq cache in the presence of metavariables 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
#8883 opened Jun 19, 2025 by JovanGerb • Draft
1
feat: links libidn2 toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8871 opened Jun 18, 2025 by algebraic-dev • Draft
@algebraic-dev
1
feat: complete level def eq 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
#8867 opened Jun 18, 2025 by Rob23oba • Draft
4
fix: walk through types of axioms in collectAxioms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8842 opened Jun 17, 2025 by Hagb • Draft
1
3
draft: range migration test run
#8841 opened Jun 17, 2025 by datokrat • Draft
ProTip! Mix and match filters to narrow down what you’re looking for.
0