Skip to content

Issues: leanprover-community/lean-auto

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
8 Open 11 Closed
8 Open 11 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

LamTerm.betaBounded bug
#38 by JOSHCLUNE was closed Nov 24, 2024
Issue with auto.native
#37 by threonorm was closed Nov 24, 2024
1
Sexp parser seemingly broken in update from Lean 4.9 to 4.11
#29 by ymherklotz was closed Sep 25, 2024
1
bump to 4.8.0-rc1
#25 by AdrienChampion was closed Jun 24, 2024
3
Lean Auto fails to translate some type classes
#22 by volodeyka was closed Apr 5, 2024
1
Faulty translation of Nat existentials into SMT
#15 by dranov was closed Feb 15, 2024
1
LT and LE for bitvectors
#10 by shigoel was closed Jan 14, 2024
3
Feature request: configuration option to write generated SMT commands to a file instead of being displayed on stdout
#9 by shigoel was closed Dec 14, 2023
4
Feature request: configuration option to allow the user to change solver timeouts
#8 by shigoel was closed Dec 14, 2023
2
Bug in the translation of Std.BitVec.not
#6 by shigoel was closed Dec 7, 2023
@PratherConid
2
Feature request: SMT trigger annotations
#3 by atomb was closed Apr 16, 2024
1
ProTip! Find all open issues with in progress development work with linked:pr.