search

abella-prover / abella

An interactive theorem prover based on lambda-tree syntax
https://abella-prover.org/
GNU General Public License v3.0
89 stars 18 forks source link

Improving Not_found error message #51

Closed lambdacalculator closed 8 years ago

lambdacalculator commented 8 years ago

If I use the tactic apply theorem_name to H1 H2 H3 H4 H5 H6 H7 H8 H9 H10 and I get Error: Not_found, I don't know immediately whether that's because I misspelled or used a non-existent theorem or hypothesis.

For convenience, the error message should include the offending identifier.

chaudhuri commented 8 years ago

Thanks for this report. I had already swept through Abella trying to kill as many of these naked exceptions as possible, but I have clearly not been exhaustive. Please complain loudly and often whenever you see such exceptions, especially if they don't give much of a hint of what needs to be fixed.