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

Split on unknown id produces OCaml exception #64

Closed lambdacalculator closed 8 years ago

lambdacalculator commented 8 years ago

Welcome to Abella 2.0.4-b1 Abella < Split a as b,c. Error: Not_found

Sorry for displaying a naked OCaml exception. An informative error message has not been designed for this situation.

To help improve Abella's error messages, please file a bug report at https://github.com/abella-prover/abella/issues. Thanks!

lambdacalculator commented 8 years ago

Also happens in one other case where an ID is expected but an unknown one is given:

Welcome to Abella 2.0.4-b1 Abella < Show a. Error: Not_found

Sorry for displaying a naked OCaml exception. An informative error message has not been designed for this situation.

To help improve Abella's error messages, please file a bug report at https://github.com/abella-prover/abella/issues. Thanks!