The Coq mailing list

[Roman Beslik <beroal AT ukr.net>]

On 19.03.10 04:26, Gyesik Lee wrote:
> b) How to overcome the termination check in proof mode when using
> well-founded (structural) relation as in the fourth attempt?
>    
First, Coq thinks that structural argument is "a". Because of "match x", 
I suppose that structural argument is "x", so write it explicitly: "fix 
to_T (a : Rep) (x : Interpret RT a) {struct x} : ...". Then you must 
call "to_T" with a subterm of "x". That subterm is of type "Interpret RT 
Rec". "to_T" may not receive an argument of such a type, so you can not 
call "to_T". Recursion is impossible.
And it does not make sense to me. What do you suppose "to_T" to do?

--
Best regards,
  Roman Beslik.