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

592 Open 1,368 Closed
592 Open 1,368 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

unused variable FP with forall syntax in signature bug Something isn't working
#6201 opened Nov 24, 2024 by digama0
RFC: Visual Separators in Number Literals RFC Request for comments
#6199 opened Nov 24, 2024 by Command-Master
1
3
lake: seems to accumulate "././"s with dependencies bug Something isn't working
#6186 opened Nov 23, 2024 by juhp
2 of 3 tasks
cmake should make use of pkgconfig to detect shared libuv and gmp libs correctly bug Something isn't working
#6183 opened Nov 23, 2024 by juhp
1 task done
conv-mode congr leaves unsynthesized placeholder bug Something isn't working
#6179 opened Nov 22, 2024 by eric-wieser
3 tasks done
RFC: pretty printing dot notation with CoeFun RFC Request for comments
#6178 opened Nov 22, 2024 by edegeltje
Confusing crash on infinite loop in metaprogram bug Something isn't working
#6172 opened Nov 22, 2024 by david-christiansen
Our RNG interface and implementation seem outdated
#6171 opened Nov 22, 2024 by david-christiansen
Lemma duplication ite_self and ite_id bug Something isn't working
#6169 opened Nov 22, 2024 by nomeata
simp? does not work in conv mode bug Something isn't working P-medium We may work on this issue if we find the time
#6164 opened Nov 21, 2024 by MichaelStollBayreuth
3 tasks done
1
simp? after a focus dot produces incorrectly indented lines bug Something isn't working P-low We are not planning to work on this issue
#6163 opened Nov 21, 2024 by MichaelStollBayreuth
3 tasks done
simp_arith: unwanted reduction of atoms due to overloaded vs. nonoverloaded operations bug Something isn't working P-medium We may work on this issue if we find the time
#6152 opened Nov 21, 2024 by nomeata
2
Sum.elim_map should be simp bug Something isn't working P-medium We may work on this issue if we find the time
#6142 opened Nov 20, 2024 by nomeata
1 of 3 tasks
Lean's LSP internals appear in autocompletes for IO.FS.Stream bug Something isn't working P-low We are not planning to work on this issue
#6135 opened Nov 20, 2024 by david-christiansen
2
pp.all cannot round-trip applied lambdas with implicit binders bug Something isn't working P-medium We may work on this issue if we find the time
#6122 opened Nov 19, 2024 by eric-wieser
3 tasks done
parseQuotWithCurrentStage works reliably only for builtin parsers bug Something isn't working P-medium We may work on this issue if we find the time
#6118 opened Nov 18, 2024 by Kha
1
RFC: Attributes in #print P-medium We may work on this issue if we find the time RFC Request for comments
#6107 opened Nov 17, 2024 by digama0
1
2
Quotation does not detect ambiguity bug Something isn't working P-medium We may work on this issue if we find the time
#6101 opened Nov 16, 2024 by jthulhu
3 tasks done
Compiling some if constant expressions with Float causes deep recursion 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-medium We may work on this issue if we find the time
#6099 opened Nov 16, 2024 by Rob23oba
3 tasks done
1
RFC: let notation inside declaration binders P-low We are not planning to work on this issue RFC Request for comments
#6091 opened Nov 15, 2024 by eric-wieser
2
reduce does not recurse into binder types bug Something isn't working P-low We are not planning to work on this issue
#6084 opened Nov 15, 2024 by JLimperg
3 tasks done
Binder can't update to typeclass argument bug Something isn't working P-medium We may work on this issue if we find the time
#6078 opened Nov 14, 2024 by YaelDillies
3 tasks done
RFC: give linters access to all the syntax up to the current command P-medium We may work on this issue if we find the time RFC Request for comments
#6076 opened Nov 14, 2024 by adomani
4
Linear code leads to non-linear IR 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
#6058 opened Nov 13, 2024 by TwoFX
3 tasks done
RFC: Recording of Open Namespaces P-medium We may work on this issue if we find the time RFC Request for comments
#6050 opened Nov 12, 2024 by hargoniX
1
ProTip! Follow long discussions with comments:>50.