Skip to content

Pull requests: leanprover/lean4

New pull request New
205 Open 4,700 Closed
205 Open 4,700 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: lake: support plugins changelog-lake Lake release-ci Enable all CI checks for a PR, like is done for releases
#7001 opened Feb 9, 2025 by tydeu • Draft
fix: prevent compiler crash in casesOn optimization toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6993 opened Feb 7, 2025 by Rob23oba Loading…
1
1
feat: allow turnstiles anywhere in location sequences changelog-language Language features, tactics, and metaprograms changes-stage0 Contains stage0 changes, merge manually using rebase
#6992 opened Feb 7, 2025 by jrr6 Loading…
1
13
chore: build Lean with Elab.async toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6989 opened Feb 7, 2025 by Kha Loading…
3
chore: don't forget about namespace reservation for async-unsupported constant kinds toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6987 opened Feb 7, 2025 by Kha Loading…
@nomeata
1
feat: add BitVec.(getElem, getLsbD, getMsbD, msb)_smod theorems toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6986 opened Feb 7, 2025 by luisacicolini • Draft
1
chore: re-enable Elab.async on the cmdline 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
#6985 opened Feb 7, 2025 by Kha • Draft
9
fix: FileSystem.normalize toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6983 opened Feb 7, 2025 by neunenak Loading…
1
doc: standard library design principles changelog-doc Documentation toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6974 opened Feb 6, 2025 by TwoFX • Draft
1
perf: dsimp shouldn't visit proofs 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
#6973 opened Feb 6, 2025 by JovanGerb • Draft
1
1
feat: verify toList for hash maps toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6954 opened Feb 5, 2025 by jt0202 • Draft
8
feat: add BitVec.umulOverflow and BitVec.smulOverflow definitions and additional theorems toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6949 opened Feb 4, 2025 by luisacicolini • Draft
5
feat: basic support for handling enum inductives in bv_decide 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
#6946 opened Feb 4, 2025 by hargoniX • Draft
1
fix: make name unresolution consistent and avoid auxiliary names 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
#6938 opened Feb 4, 2025 by jrr6 • Draft
1
1
feat: staged CMake build with Lake as a plugin 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
#6929 opened Feb 3, 2025 by tydeu Loading…
5
fix: make extern decls evaluate as ⊤ instead of ⊥ in LCNF.elimDeadBranches changelog-compiler Compiler, runtime, and FFI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6928 opened Feb 3, 2025 by zwarich Loading…
1
feat: tree map data structures and operations 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
#6914 opened Feb 3, 2025 by datokrat Loading…
72
fix: set iota := true in simpGlobalConfig 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
#6909 opened Feb 3, 2025 by JovanGerb Loading…
1
2
feat: simp diagnostics in grind changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6902 opened Feb 1, 2025 by leodemoura Loading…
1
feat: lake: async imports breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-lake Lake toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6894 opened Feb 1, 2025 by tydeu • Draft
1
fix: incremental goal state requests select incomplete snapshot
#6887 opened Jan 31, 2025 by mhuisi Loading…
1
8
feat: containsThenInsertIfNew for the tree map changes-stage0 Contains stage0 changes, merge manually using rebase
#6867 opened Jan 30, 2025 by datokrat • Draft
feat: insertIfNew for the tree map changes-stage0 Contains stage0 changes, merge manually using rebase toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6865 opened Jan 30, 2025 by datokrat • Draft
1
feat: containsThenInsert for the tree map changes-stage0 Contains stage0 changes, merge manually using rebase toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6857 opened Jan 29, 2025 by datokrat • Draft
1
feat: size and erase for the tree map changes-stage0 Contains stage0 changes, merge manually using rebase toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#6850 opened Jan 29, 2025 by datokrat • Draft
1
ProTip! Mix and match filters to narrow down what you’re looking for.