Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

#

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Jump to bottom

Unsuccessful proof search shouldn't just increase the hole number #199

Closed
turion opened this issue Dec 17, 2017 · 0 comments
Closed

Unsuccessful proof search shouldn't just increase the hole number #199

turion opened this issue Dec 17, 2017 · 0 comments

Comments

@turion
Copy link

turion commented Dec 17, 2017

Assume I have code like this:

proof : hardStatement
proof = ?proof_rhs1

Now press ctrl-alt-s while focussing on ?proof_rhs1. If it doesn't find a term for the hole, it just replaces it by ?proof_rhs2. It would be more useful not to rename the hole and instead give an error message.
justjoheinz pushed a commit to justjoheinz/atom-language-idris that referenced this issue Sep 12, 2018
Improve proof search
7075b26 
When the result of the proof search returns an :ok message starting
with a ?, display that the proof search was not succesful, otherwise
insert the found proof.

Fixes idris-hackers#199
@justjoheinz justjoheinz mentioned this issue Sep 12, 2018
Merged
# for free to join this conversation on GitHub. Already have an account? # to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@turion