Skip to content

Pull requests: leanprover/lean4

New pull request New
134 Open 2,495 Closed
134 Open 2,495 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: better job captions & log grouping
backport releases/v4.8.0 toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#4115 opened May 9, 2024 by tydeu • Draft v4.8.0-rc2
1
1
fix: type class 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
#4114 opened May 9, 2024 by leodemoura Loading…
3
2
fix: lake: TOML key order bug in ppTable
backport releases/v4.8.0 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
#4104 opened May 8, 2024 by tydeu Loading… v4.8.0-rc2
1
1
feat: IO.TaskState
backport releases/v4.8.0 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
#4097 opened May 7, 2024 by tydeu Loading… v4.8.0-rc2
4
chore: tidying up Lean.unresolveNameGlobal
toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#4091 opened May 7, 2024 by kmill Loading…
1
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: add BitVec.[toInt_inj|toInt_ne]
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
#4075 opened May 6, 2024 by tobiasgrosser Loading…
@semorrison
4
feat: well-founded definitions irreducible by default
builds-mathlib CI has verified that Mathlib builds against this PR full-ci Run full CI suite toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN will-merge-soon …unless someone speaks up
#4061 opened May 3, 2024 by nomeata Loading…
1
7
chore: modernize build instructions
full-ci Run full CI suite toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#4032 opened Apr 30, 2024 by Kha Loading…
4
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
chore: add dates to @[deprecated] attributes
toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#3967 opened Apr 22, 2024 by semorrison Loading…
2
fix: validate UTF-8 at C++ -> Lean boundary
full-ci Run full CI suite toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#3963 opened Apr 20, 2024 by digama0 Loading…
27
feat: incremental elaboration of definition headers, bodies, and tactics
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
#3940 opened Apr 18, 2024 by Kha • Draft
6
feat: rm partial / bounds checks in Array.qsort
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.
#3933 opened Apr 17, 2024 by digama0 Loading…
11
feat: apply’s error message should show implicit arguments as needed
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
#3929 opened Apr 16, 2024 by nomeata Loading…
1
12
feat: make binder predicates use strict-implicit binders
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
#3928 opened Apr 16, 2024 by kmill • Draft
1
feat: @[builtin_doc] attribute (part 2)
builds-mathlib CI has verified that Mathlib builds against this PR full-ci Run full CI suite toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#3918 opened Apr 15, 2024 by digama0 Loading…
10
feat: display auto-implicits as inlay hints
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
#3910 opened Apr 15, 2024 by Kha • Draft
3
feat: make frontend normalize line endings to LF
toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#3903 opened Apr 14, 2024 by kmill Loading…
11
feat: support Lake for building Lean core oleans
full-ci Run full CI suite toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#3886 opened Apr 12, 2024 by david-christiansen Loading…
@tydeu
6
feat: binary recursive implementation of List.mapA
awaiting-author Waiting for PR author to address issues 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
#3877 opened Apr 11, 2024 by digama0 Loading…
5
feat: complete Int div/mod simprocs
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
#3850 opened Apr 9, 2024 by joehendrix Loading…
1
ProTip! Filter pull requests by the default branch with base:master.