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

634 Open 1,456 Closed
634 Open 1,456 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

lake: import error points at wrong line bug Something isn't working
#7065 opened Feb 13, 2025 by RalfJung
3 tasks done
RFC: add BitVec.eq_of_getElem_eq as BitVec ext lemma RFC Request for comments
#7045 opened Feb 12, 2025 by JamesGallicchio
RFC: late fixed parameters in functional induction P-high We will work on this issue RFC Request for comments
#7027 opened Feb 10, 2025 by nomeata
@nomeata
lake update output is inconsistent between path and Git dependencies bug Something isn't working P-low We are not planning to work on this issue
#7025 opened Feb 10, 2025 by david-christiansen
Valid list index is rejected bug Something isn't working P-medium We may work on this issue if we find the time
#6999 opened Feb 8, 2025 by Vtec234
dsimp unfolds definition in post-phase, not pre-phase bug Something isn't working P-low We are not planning to work on this issue
#6969 opened Feb 6, 2025 by nomeata
RFC: dsimp should not simplify proofs P-low We are not planning to work on this issue RFC Request for comments
#6960 opened Feb 5, 2025 by JovanGerb
1
4
using Option.attach can crash lean 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 P-high We will work on this issue
#6957 opened Feb 5, 2025 by Rob23oba
3 tasks done
1
1
Unknown free variable '_fvar.639' bug Something isn't working P-medium We may work on this issue if we find the time
#6927 opened Feb 3, 2025 by dplyukhin
3 tasks done
1
Info view term hover shows field notation docs instead of docstring of hovered constant bug Something isn't working P-medium We may work on this issue if we find the time
#6906 opened Feb 2, 2025 by Kha
3 tasks done
1
RFC: Allow doc comments in standalone deriving awaiting-author Waiting for PR author to address issues RFC Request for comments
#6896 opened Feb 1, 2025 by alok
2
RFC: open keyword in do-monad P-low We are not planning to work on this issue RFC Request for comments
#6884 opened Jan 31, 2025 by neunenak
1
RFC: attribute induction_case_names P-medium We may work on this issue if we find the time RFC Request for comments
#6874 opened Jan 30, 2025 by nomeata
@nomeata
RFC: Lake update stable P-medium We may work on this issue if we find the time RFC Request for comments
#6843 opened Jan 29, 2025 by madvorak
Compilation of large inductive type definition takes ~20mins bug Something isn't working P-low We are not planning to work on this issue
#6820 opened Jan 28, 2025 by tothtamas28
3 tasks done
2
linux_wasm32 libleanrt.a seems to incorrectly refer to libuv symbols bug Something isn't working P-low We are not planning to work on this issue pr-welcome A PR from an external contributor, implementing the RFC as described, would be welcome.
#6817 opened Jan 28, 2025 by ianh
2 of 3 tasks
1
RFC: introduce notations for Duration and Timestamp and remove dangerous OfNat instances P-medium We may work on this issue if we find the time RFC accepted RFC is waiting for a corresponding PR (external or internal) RFC Request for comments
#6793 opened Jan 27, 2025 by TwoFX
2
Issues with default parameters bug Something isn't working P-low We are not planning to work on this issue
#6769 opened Jan 24, 2025 by imbrem
3 tasks done
@kmill
Lean server keeps consuming more memory as it reprocesses a large definition bug Something isn't working P-medium We may work on this issue if we find the time
#6753 opened Jan 23, 2025 by pandaman64
3 tasks done
3
sorry source is displayed in infoview with let bug Something isn't working P-medium We may work on this issue if we find the time
#6715 opened Jan 20, 2025 by edegeltje
3 tasks done
@kmill
exact? suggests an extra id bug Something isn't working P-low We are not planning to work on this issue
#6710 opened Jan 20, 2025 by ldct
3 tasks done
1
simp? can still incorrectly unresolve a name to the current theorem name bug Something isn't working P-medium We may work on this issue if we find the time
#6706 opened Jan 20, 2025 by mniip
1
3
exact? configuration option to consider otherwise ignored, internal theorems enhancement New feature or request P-low We are not planning to work on this issue
#6673 opened Jan 16, 2025 by kim-em
1
exact? fails to close goal bug Something isn't working P-medium We may work on this issue if we find the time
#6666 opened Jan 16, 2025 by TwoFX
3 tasks done
simp? unfolds more let definitions than a bare simp call bug Something isn't working P-medium We may work on this issue if we find the time
#6655 opened Jan 15, 2025 by sgouezel
3 tasks done
3
ProTip! Updated in the last three days: updated:>2025-02-10.