Skip to content

Pull requests: leanprover/lean4

New pull request New
140 Open 2,597 Closed
140 Open 2,597 Closed
Author
Filter by author
Label
Filter by label
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Milestones
Filter by milestone
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 test improvements & lake lint
#4261 opened May 23, 2024 by tydeu • Draft
3
feat: make <num>#<num> bitvector literal notation global
toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#4260 opened May 23, 2024 by leodemoura Loading…
3
doc: add docstrings for dsimp configuration
awaiting-review Waiting for someone to review the PR documentation Documentation improvement toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#4258 opened May 23, 2024 by kmill Loading…
1
feat: getLsb_{rotateLeft, rotateRight}
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
#4257 opened May 23, 2024 by bollu Loading…
12
feat: widget messages
toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#4254 opened May 23, 2024 by Vtec234 Loading…
1
1
chore: minimization of variable-induced slowdown
toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#4253 opened May 23, 2024 by semorrison Loading…
1
feat: add missing theorems for + 1 and - 1 normal form
awaiting-author Waiting for PR author to address issues breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan full-ci Run full CI suite toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#4242 opened May 21, 2024 by markusschmaus Loading…
12
fix: add inc for double resets
toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#4228 opened May 20, 2024 by anfelor Loading…
1
chore: decrease priority for MonadError
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
#4223 opened May 19, 2024 by JovanGerb • Draft
1
1
chore: fix the MonadStore type classes, with semiOutParam
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
#4205 opened May 17, 2024 by JovanGerb Loading…
16
chore: add minimization for 'dsimp at' issue
toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#4198 opened May 17, 2024 by semorrison • Draft
1
feat: getLsb_signExtend
#4187 opened May 16, 2024 by bollu • Draft
1
feat: getLsb_sshiftRight
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
#4179 opened May 15, 2024 by bollu Loading…
37
feat: simp to still work even if one simp arg does not work
awaiting-review Waiting for someone to review the PR new-user-papercuts Issue likely to confuse or otherwise negatively affect new users, even if only a little toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#4177 opened May 15, 2024 by nomeata Loading…
7
feat: test for simp problem
toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#4171 opened May 15, 2024 by semorrison • Draft
3
refactor: DiscrTree: return more specific results first
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
#4158 opened May 14, 2024 by nomeata • Draft
8
feat: fine-grained equational lemmas for non-recursive equations
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
#4154 opened May 13, 2024 by nomeata • Draft
1
perf: globally cache intermediate type class results
breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan full-ci Run full CI suite toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#4152 opened May 13, 2024 by JovanGerb • Draft
10
fix: FunInd: Introduce HEq where necessary and no equality on Props
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
#4149 opened May 13, 2024 by nomeata Loading…
1
1
chore: CI: optimize code under Linux Debug
full-ci Run full CI suite toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#4118 opened May 9, 2024 by Kha • Draft
2
refactor: lake: manifest semver & code cleanup
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 will-merge-soon …unless someone speaks up
#4083 opened May 6, 2024 by tydeu Loading…
5
feat: lake install
#3998 opened Apr 26, 2024 by tydeu • Draft
1
3
experiment: split PHashMap / PHashMapSized
toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#3997 opened Apr 26, 2024 by digama0 • Draft
1
feat: Implement Functor for Array
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
#3976 opened Apr 23, 2024 by alok • Draft
6
feat: use rfl proofs of Iff in dsimp
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 WIP This is work in progress, and only a PR for the sake of CI or sharing. No review yet.
#3973 opened Apr 23, 2024 by thorimur • Draft
2
ProTip! Adding no:label will show everything without a label.