Skip to content
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

Pick the goal of a theorem in a smarter way #14

Open
leotrs opened this issue Feb 19, 2022 · 1 comment
Open

Pick the goal of a theorem in a smarter way #14

leotrs opened this issue Feb 19, 2022 · 1 comment

Comments

@leotrs
Copy link
Owner

leotrs commented Feb 19, 2022

Currently the first claim found in the body of a theorem is chosen as the goal. We need to do better. First, if the theorem contains a ASSUME/PROVE clause, then the claim following PROVE should be chosen as the goal. Other than that, a good heuristic is to choose the last claim, not the first.

What to do with theorems that make multiple statements?

@leotrs
Copy link
Owner Author

leotrs commented Feb 19, 2022

Remember an ordinary claim is equivalent to an ASSUME/PROVE clause with an empty ASSUME part.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant