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

513 Open 997 Closed
513 Open 997 Closed
Author
Filter by author
Label
Filter by label
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Milestones
Filter by milestone
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

termination_by? over generalizes the decreasing term bug Something isn't working
#4230 opened May 20, 2024 by hargoniX
3 tasks done
@nomeata
1
RFC: merging the notions of outParam and semiOutParam RFC Request for comments
#4225 opened May 20, 2024 by JovanGerb
The execution of IO actions can cause flaky builds bug Something isn't working
#4214 opened May 18, 2024 by gaborcs
3 tasks done
6
RFC: type class synthesis order when outParam has multiple possible values RFC Request for comments
#4212 opened May 18, 2024 by JovanGerb
1
1
Fails to compile stage2 on msys2/mingw64 bug Something isn't working
#4197 opened May 17, 2024 by Kreijstal
3 tasks done
1
@[inline] annotation is ignored when specializing function with fixed type class argument bug Something isn't working
#4191 opened May 16, 2024 by TwoFX
3 tasks done
RFC: No goals should point to errors elsewhere RFC Request for comments
#4190 opened May 16, 2024 by fpvandoorn
3
RFC: mutual structures RFC Request for comments
#4182 opened May 15, 2024 by ice1000
6
RFC: show robust tactic state RFC Request for comments
#4181 opened May 15, 2024 by fpvandoorn
2
simp should try more specific lemmas first
#4173 opened May 15, 2024 by nomeata
non-exported lean_libs in Lake feature missing feature Lake Lake related issue
#4168 opened May 15, 2024 by semorrison
Lake build fails on Windows when issuing long command line bug Something isn't working Lake Lake related issue
#4159 opened May 14, 2024 by bernborgess
2 of 3 tasks
Inferred value for implicit argument leads to suboptimal IR bug Something isn't working
#4157 opened May 14, 2024 by TwoFX
3 tasks done
Unexpected token mutual after docstring comment bug Something isn't working
#4156 opened May 13, 2024 by ionathanch
3 tasks done
1
FunInd chokes on pattern match with dependent targets bug Something isn't working
#4146 opened May 13, 2024 by nomeata
1
Allowing adding testRunner = true to a lean_lib in lakefile.toml. feature missing feature Lake Lake related issue
#4142 opened May 12, 2024 by semorrison
5
Raw kernel "invalid return type" error upon extending typeclass with unquantified type variable bug Something isn't working
#4140 opened May 12, 2024 by bollu
3 tasks done
Suggestion on Document: Explicit Declaration for Multiple Universe Level Variable
#4122 opened May 10, 2024 by DKXXXL
@david-christiansen
3
allow using an upstream executable as a lake @[test_runner] feature missing feature Lake Lake related issue
#4121 opened May 10, 2024 by semorrison
inherit_doc does not show docs on the declaration itself bug Something isn't working
#4204 opened May 9, 2024 by alok
4
lake test --help gives lakefile.lean specific instructions (i.e. not toml) documentation Documentation improvement Lake Lake related issue
#4116 opened May 9, 2024 by semorrison
@tydeu
Pattern alternative binding empty type does not cause redundant alternative warning bug Something isn't working
#4110 opened May 8, 2024 by lovely-error
10
lake translate-config does not give a helpful error message feature missing feature Lake Lake related issue
#4107 opened May 8, 2024 by semorrison
@tydeu
2
lake new should generate a lakefile.toml, not a lakefile.lean Lake Lake related issue new-user-papercuts Issue likely to confuse or otherwise negatively affect new users, even if only a little RFC Request for comments
#4106 opened May 8, 2024 by semorrison
lake should give a warning when it looks like nothing is imported, by accident Lake Lake related issue new-user-papercuts Issue likely to confuse or otherwise negatively affect new users, even if only a little RFC Request for comments
#4105 opened May 8, 2024 by semorrison
@tydeu
4
ProTip! Type g p on any issue or pull request to go back to the pull request listing page.