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

Lack of error message #79

Closed lambdacalculator closed 7 years ago

lambdacalculator commented 7 years ago

Trying to do a mutual induction on the wrong number of propositions produces a naked OCaml exception:

Kind unit type.
Define p : unit -> prop by p U.

Theorem mutual : (forall U, p U -> p U) /\ (forall U, p U -> p U).
induction on 1.  % or induction on 1 1 1.

produces the message

Error: Invalid_argument("List.combine")

 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!