Skip to content

Pull requests: leanprover/lean4

New pull request New
227 Open 5,044 Closed
227 Open 5,044 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: only log goals accomplished in language server changelog-no Do not include this PR in the release changelog
#7416 opened Mar 10, 2025 by mhuisi Loading…
feat: BitVec conversion lemmas changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7415 opened Mar 10, 2025 by TwoFX Loading…
1
feat: remaining lemmas about iterated conversions of finite types changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7414 opened Mar 10, 2025 by TwoFX Loading…
1
chore: add highlights for v4.18 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
#7413 opened Mar 10, 2025 by eyihluyc • Draft
2
feat: new tree map lemmas for getKey changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7412 opened Mar 10, 2025 by datokrat • Draft
1
fix: make the Subsingleton instance for Squash work for an arbitrary Sort 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
#7406 opened Mar 9, 2025 by cppio Loading…
1
2
feat: hash map lemmas for filter, map and filterMap toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7400 opened Mar 8, 2025 by Rob23oba • Draft
1
fix: change 'show' tactic to work as documented toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7395 opened Mar 8, 2025 by Rob23oba • Draft
1
feat: lake: config field autocomplete in whitespace 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
#7393 opened Mar 8, 2025 by tydeu Loading…
1
doc: revise show tactic documentation to more accurately describe its behavior toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7389 opened Mar 7, 2025 by euprunin Loading…
9
fix: find realizations from other env branches awaiting-mathlib We should not merge this until we have a successful Mathlib build builds-mathlib CI has verified that Mathlib builds against this PR changelog-no Do not include this PR in the release changelog force-mathlib-ci toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7385 opened Mar 7, 2025 by Kha Loading…
10
feat: make more constructions async-compatible builds-mathlib CI has verified that Mathlib builds against this PR changelog-no Do not include this PR in the release changelog force-mathlib-ci toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7384 opened Mar 7, 2025 by Kha • Queued
3
refactor: the AIG framework to track negations in a more efficient way changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7381 opened Mar 7, 2025 by hargoniX • Draft
5
feat: tree map lemmas for modify changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7379 opened Mar 7, 2025 by datokrat Loading…
2
fix: use getElem instead of get in the statements of hash map lemmas changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7377 opened Mar 7, 2025 by datokrat Loading…
1
doc: manual docstring review for smaller namespaces changelog-doc Documentation toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7365 opened Mar 6, 2025 by david-christiansen • Draft
1
feat: auxLemmaNames to use enterable names 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
#7364 opened Mar 6, 2025 by nomeata • Draft
1
feat: lemmas about pure for {List,Array,Vector}.{mapM,foldlM,foldrM,anyM,allM,findM?,findSomeM?} changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7356 opened Mar 6, 2025 by eric-wieser Loading…
3
fix: replace bad simp lemmas for Id changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7352 opened Mar 5, 2025 by eric-wieser • Draft
3
fix: handle macro scopes and hover info in exact? output builds-mathlib CI has verified that Mathlib builds against this PR 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
#7349 opened Mar 5, 2025 by jrr6 • Draft
3
chore: unconditionally re-enable realizeConst 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 force-mathlib-ci toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7334 opened Mar 4, 2025 by Kha Loading…
1
chore: fix spelling mistakes 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
#7328 opened Mar 4, 2025 by euprunin Loading…
2
fix: indenting in release notes script toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7326 opened Mar 4, 2025 by kim-em Loading…
1
fix: make new codegen async realization-compatible 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
#7316 opened Mar 4, 2025 by Kha Loading…
3
feat: (experiment) have synth order defer "mixin" instances 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
#7313 opened Mar 4, 2025 by kmill • Draft
1
ProTip! Type g p on any issue or pull request to go back to the pull request listing page.