Skip to content

Issues: leanprover/lean4

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Clear current search query, filters, and sorts
39 Open 639 Closed
39 Open 639 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
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

fix: Make split work with metavariables in the target changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8437 opened May 21, 2025 by sgraf812 Loading…
2
feat: dot auto-completion for most occurrences of global identifiers builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features, tactics, and metaprograms release-ci Enable all CI checks for a PR, like is done for releases toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8424 opened May 20, 2025 by Rob23oba Loading…
1
1
feat: explicit rfl attribute builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features, tactics, and metaprograms 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
#8419 opened May 20, 2025 by nomeata • Draft
2 tasks
2
feat: support for lambda expressions in discr trees breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-language Language features, tactics, and metaprograms closing soon This issue will be closed soon (<1 month) as it is missing essential features. toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8395 opened May 18, 2025 by Rob23oba Loading…
4
feat: improve error behavior of end command 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
#8387 opened May 16, 2025 by jrr6 Loading…
2
feat: Meta.letToHave 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
#8373 opened May 16, 2025 by kmill Loading…
1
Experiments with metavar error reporting changelog-language Language features, tactics, and metaprograms
#8307 opened May 12, 2025 by kmill • Draft
fix: invalid dotted identifier notation error for sort changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8260 opened May 8, 2025 by tydeu Loading…
2
fix: invalid field notation error for mvar changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8259 opened May 8, 2025 by tydeu Loading…
1
fix: nested try-catch parsing builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features, tactics, and metaprograms P-high We will work on this issue toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8252 opened May 6, 2025 by Rob23oba Loading…
1
6
feat: guard against synthetic sorry misuse backport releases/v4.20.0 changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8230 opened May 5, 2025 by Kha • Draft
2
fix: record fvar alias info for generalized variables in induction/cases 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
#8002 opened Apr 17, 2025 by kmill Loading…
1
1
feat: in app elaborator, beta reduce when substituting arguments 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
#7991 opened Apr 17, 2025 by kmill • Draft
1
perf: update to cadical 2.2.0 changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7942 opened Apr 13, 2025 by hargoniX • Draft
4 tasks
8
feat: (experiment) use low priority for parent instances 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
#7894 opened Apr 10, 2025 by kmill • Draft
1
perf: add a bitblasting cache for bv_decide's boolean substructure changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7707 opened Mar 28, 2025 by hargoniX Loading…
3
feat: allow a general evalTac at evalSepTactics changelog-language Language features, tactics, and metaprograms P-medium We may work on this issue if we find the time toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7702 opened Mar 27, 2025 by JovanGerb Loading…
5
fix: allow arbitrary sorts in structural recursion over reflexive inductive types changelog-language Language features, tactics, and metaprograms P-low We are not planning to work on this issue toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7639 opened Mar 22, 2025 by cppio Loading…
1
2
fix: use pi_congr instead of forall_congr; deprecate the latter changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7577 opened Mar 19, 2025 by sgraf812 Loading…
1
8
feat: kernel: lazy_delta_reduction: try to reduce_nat 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
#7545 opened Mar 18, 2025 by nomeata • Draft
5
fix: use withFreshZetaDeltaFVarIds to avoid leaking zetaDeltaFVarIds between different simp calls builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features, tactics, and metaprograms P-low We are not planning to work on this issue toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7539 opened Mar 18, 2025 by JovanGerb Loading…
1
1
feat: run_macro & run_cmd_macro 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
#7524 opened Mar 17, 2025 by tydeu Loading…
1
feat: let synth order checker detect generalized projections 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
#7310 opened Mar 3, 2025 by kmill • Draft
1
feat: try more specific matches first in simp 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
#7195 opened Feb 23, 2025 by JovanGerb • Draft
3
feat: abstract proofs in all declaration types 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
#7181 opened Feb 21, 2025 by kmill • Draft
1
ProTip! What’s not been updated in a month: updated:<2025-04-21.