Hi, I'm trying to understand the functionalities of coq-ltac-iter through running through your example.v file. However in the last example of Iterating Premises, it returns the error message below:
Error: Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/.
At the same time, would also like to check with you on my understanding of this coq plugin. From what I conclude, this plugin allows iterating over terms found in a type. But does this iteration merely provide a reference for the user, or it allows the user to run through this iteration to solve the goal of the user?
Hi, I'm trying to understand the functionalities of
coq-ltac-iterthrough running through yourexample.vfile. However in the last example ofIterating Premises, it returns the error message below:At the same time, would also like to check with you on my understanding of this coq plugin. From what I conclude, this plugin allows iterating over terms found in a type. But does this iteration merely provide a reference for the user, or it allows the user to run through this iteration to solve the goal of the user?
Thanks.