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

Evaluation goes past cursor #24

Open
spaanse opened this issue Oct 15, 2021 · 1 comment
Open

Evaluation goes past cursor #24

spaanse opened this issue Oct 15, 2021 · 1 comment

Comments

@spaanse
Copy link

spaanse commented Oct 15, 2021

Take the following incomplete proof (the | marking my cursor)

Lemma nat_not_negative : forall i : nat, ~(i < 0) .
Proof.
   intro i. |
Qed.

Note the space between the . and my cursor. If you then instruct the plugin to evaluate to the cursor it will also evaluate the Qed, and then complains the proof is incomplete. This seems to be caused by the fact that the evaluate to cursor doesn't consider where the check will end up after evaluating one extra statement, instead it just checks if we are still before the cursor. So unless the cursor is right after the . it will always evaluate an extra statement.

@spaanse
Copy link
Author

spaanse commented Oct 15, 2021

Suggestion for a fix:

- if manager.autorun_forward and manager.position < manager.autorun_point:
+ if manager.autorun_forward and self._find_statement().end() < manager.autorun_point:

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