Skip to content

Issues: leanprover-community/aesop

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.

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

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

Issues list

Linter for inductive/structure rules
#172 opened Oct 28, 2024 by JLimperg
Negative rules
#170 opened Oct 28, 2024 by JLimperg
Avoid dependency on Std
#120 opened Mar 28, 2024 by JLimperg
Add forced and promoted subgoals
#114 opened Feb 28, 2024 by JLimperg
Can't erase simprocs
#113 opened Feb 27, 2024 by JLimperg
Fast forward rules
#111 opened Feb 21, 2024 by JLimperg
Fatal rules
#109 opened Feb 15, 2024 by JLimperg
Don't use implDetail hypotheses
#108 opened Feb 14, 2024 by JLimperg
Aesop ruleset runs forever
#94 opened Jan 7, 2024 by adomasbaliuka
aesop ignores @[eliminator]
#59 opened Jun 14, 2023 by kim-em
Rule suggestion: elim *
#19 opened Jun 27, 2022 by Kha
Ideas on dealing with quantifiers
#5 opened Nov 18, 2021 by suhr
ProTip! Type g p on any issue or pull request to go back to the pull request listing page.