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
61 Open 79 Closed
61 Open 79 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
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

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
Make rcases use the induction/cases framework enhancement New feature or request P-medium We may work on this issue if we find the time
#3901 opened Apr 13, 2024 by kmill
1
try_for tactic (timeouts in tactics) enhancement New feature or request P-low We are not planning to work on this issue
#3812 opened Mar 31, 2024 by digama0
6
Completion of keywords into identifiers enhancement New feature or request new-user-papercuts Issue likely to confuse or otherwise negatively affect new users, even if only a little P-medium We may work on this issue if we find the time server Affects the Lean server code
#3623 opened Mar 6, 2024 by Kha
@mhuisi
9
[question] How to write the 'require' line in lakefile.lean to use the pre-installed Lean library? enhancement New feature or request Lake Lake related issue P-medium We may work on this issue if we find the time
#3193 opened Jan 17, 2024 by yurivict
9
lake update silently fails when argument does not exists bug Something isn't working enhancement New feature or request Lake Lake related issue P-high We will work on this issue
#2772 opened Oct 26, 2023 by PatrickMassot
1 task done
Make use of Top Byte Ignore on AArch64 enhancement New feature or request low priority P-low We are not planning to work on this issue
#2437 opened Aug 20, 2023 by Kha
@zwarich
3
[RFC] JSON package / library config info output enhancement New feature or request Lake Lake related issue P-medium We may work on this issue if we find the time performance A performance problem related issue or PR
#2753 opened Jul 8, 2023 by digama0
10
Do not report expected type when not helpful enhancement New feature or request P-medium We may work on this issue if we find the time server Affects the Lean server code
#2202 opened Apr 25, 2023 by Kha
If inside conv enhancement New feature or request P-low We are not planning to work on this issue
#2063 opened Jan 26, 2023 by jeremysalwen
Conditional transitive dependencies are downloaded unconditionally enhancement New feature or request Lake Lake related issue P-medium We may work on this issue if we find the time
#2755 opened Jan 21, 2023 by ghost
4
Failure state writing to broken pipe enhancement New feature or request P-low We are not planning to work on this issue
#2013 opened Jan 5, 2023 by ykonstant1
1 task done
3
Option for precompiling whole packages enhancement New feature or request Lake Lake related issue P-low We are not planning to work on this issue
#2757 opened Nov 17, 2022 by Kha
lake init create a default .git directory with potientially wrong defaults enhancement New feature or request Lake Lake related issue P-medium We may work on this issue if we find the time
#2758 opened Sep 13, 2022 by fredokun
6
cases can reorder equally named hypotheses enhancement New feature or request P-low We are not planning to work on this issue
#1556 opened Sep 1, 2022 by digama0
1
Add a safe wrapper around ptrEq depends on new code generator We are currently working on a new compiler (code generator) for Lean. This issue/PR is blocked by it enhancement New feature or request P-medium We may work on this issue if we find the time
#1502 opened Aug 22, 2022 by gebner
@zwarich
3
Syntax match does not put info on variables under repetitions enhancement New feature or request P-low We are not planning to work on this issue
#1474 opened Aug 13, 2022 by digama0
1
Add ability for making server->client requests to Server.RequestM enhancement New feature or request P-low We are not planning to work on this issue server Affects the Lean server code
#1465 opened Aug 12, 2022 by Vtec234
Replace String.fromUtf8Unchecked with String.fromUtf8? enhancement New feature or request P-low We are not planning to work on this issue
#1462 opened Aug 12, 2022 by Kha
@lovettchris
3
Feature request: parametric targets in lake enhancement New feature or request Lake Lake related issue P-medium We may work on this issue if we find the time
#2759 opened Aug 9, 2022 by Vtec234
Better import errors enhancement New feature or request P-medium We may work on this issue if we find the time server Affects the Lean server code
#1438 opened Aug 7, 2022 by digama0
4
Inconsistent substitution behavior of cases enhancement New feature or request low priority P-low We are not planning to work on this issue
#1413 opened Aug 3, 2022 by Kha
2
elab_rules : tactic patterns require redundant information enhancement New feature or request
#1348 opened Jul 21, 2022 by leodemoura
2
No good way for proofs or local instances in theorem statements enhancement New feature or request
#1313 opened Jul 17, 2022 by gebner
6
lake graph enhancement New feature or request Lake Lake related issue
#2760 opened Jul 9, 2022 by hargoniX
1
ProTip! What’s not been updated in a month: updated:<2025-04-27.