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

528 Open 1,088 Closed
528 Open 1,088 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

RFC: size on disk for teaching RFC Request for comments
#4630 opened Jul 2, 2024 by PatrickMassot
Identifiers in auto-tactics don't respect lexical scope bug Something isn't working
#4624 opened Jul 2, 2024 by david-christiansen
3 tasks done
2
Incremental tactics leading to errors disappearing in proof bug Something isn't working
#4623 opened Jul 2, 2024 by ymherklotz
3 tasks done
2
textDocument/rename does not rename occurrences of hyp after tac at hyp for tac = rw, simp, etc bug Something isn't working
#4622 opened Jul 2, 2024 by llllvvuu
3 tasks done
Running simp? output produces different goal than simp bug Something isn't working
#4615 opened Jul 2, 2024 by llllvvuu
3 tasks done
2
FFI: extern opaque fails to compile bug Something isn't working
#4614 opened Jul 2, 2024 by ydewit
3 tasks done
simp doesn't rewrite in definitions because of unassigned metavariables bug Something isn't working
#4613 opened Jul 1, 2024 by fpvandoorn
3 tasks done
5
Metavariables in have's type should not leak into body bug Something isn't working
#4610 opened Jul 1, 2024 by Kha
lean-action template for lake new/init RFC Request for comments
#4606 opened Jul 1, 2024 by austinletson
1
1
lean --stdin --run ignores the first trailing argument bug Something isn't working
#4601 opened Jul 1, 2024 by Kha
simp unfolds local def through projection bug Something isn't working
#4585 opened Jun 28, 2024 by lecopivo
"Try this" suggestion includes trailing comments bug Something isn't working
#4581 opened Jun 28, 2024 by TwoFX
3 tasks done
induction_eliminator and cases_eliminator only key on the head symbol bug Something isn't working
#4577 opened Jun 27, 2024 by eric-wieser
2 of 3 tasks
possible bug in IO.FS.lines bug Something isn't working
#4573 opened Jun 27, 2024 by Seasawher
ppSpace in elab/macro is ignored before constructor dot notation bug Something isn't working
#4561 opened Jun 25, 2024 by eric-wieser
3 tasks done
1
1
Failure of exhaustiveness checker when matching on Exception bug Something isn't working
#4555 opened Jun 24, 2024 by JLimperg
3 tasks done
3
RFC: try-this widget: multiple replacemens, alternative text in InfoView RFC Request for comments
#4551 opened Jun 24, 2024 by nomeata
unknown free variable: _kernel_fresh.1210 bug Something isn't working depends on new code generator We are currently working on a new compiler (code generator) for Lean. This issue/PR is blocked by it
#4548 opened Jun 24, 2024 by nomeata
2
libStd.a file not found running nix develop through flake template bug Something isn't working low priority pr-welcome A PR from an external contributor, implementing the RFC as described, would be welcome.
#4545 opened Jun 24, 2024 by noghartt
3 tasks done
2
Consider making WorkspaceClientCapabilities.applyEdit field Optionable bug Something isn't working
#4541 opened Jun 23, 2024 by onriv
structural recursion fails in the equation compiler bug Something isn't working
#4540 opened Jun 23, 2024 by b-mehta
3 tasks done
26
GuessLex confused by decreasing_by proof that fails on “wrong” measures bug Something isn't working low priority
#4523 opened Jun 21, 2024 by nomeata
RFC: GuessLex omit source pos from error message low priority RFC Request for comments
#4519 opened Jun 21, 2024 by Seasawher
@nomeata
9
Some uint lemmas do not follow correct naming conventions bug Something isn't working
#4513 opened Jun 20, 2024 by fgdorais
1 of 3 tasks
1
Conflict with deeply nested rec function declarations bug Something isn't working
#4510 opened Jun 20, 2024 by JaafarTanoukhi
1
ProTip! Exclude everything labeled bug with -label:bug.