As shown in the figure, I define an induction type, but when I compile, the error is as follows
I don’t know why,I hope you can help me.Thanks
Are you sure that the error comes from the fragment of code you are showing? It looks like it is a report about a piece of code that matches on the classify_cmp_cases itself, not on type as in your example. Could it be that the error comes from another function?
It would be helpful if you could provide your code examples in text form rather than as pictures, so that we can copy and replay them to understand the problem. You can use
```coq
(your code here)
```
as markup syntax for syntax-highlighted blocks of Coq code.
1 Like
I’m only beginning to learn Coq myself so normally I’d let someone more experienced reply. But since you’ve been waiting a while I’ll attempt an answer based on my current limited level of knowledge.
I think the error is telling you that your match expression isn’t matching all possible forms of its two arguments. The arguments are of the form typeconv (ty:type). So to know why the match isn’t exhaustive one would need to know how typeconv and type are defined, which isn’t shown in your code snippet, and I wasn’t able to find them in the Coq reference manual, so I don’t think they’re part of the standard library.
I would suggest using the commands:
Print type.
Print typeconv.
to see how those identifiers are defined in your environment. Hopefully that will make it clear what cases your match is missing.
EDIT: I just noticed too that your code appears to have an extra vertical bar after the with.
2 Likes
It may be helpful to post enough code to reproduce the issue instead of a picture.
That’s allowed, tho not required.
sorry,that is my cursor.