The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Z wrote:
> Could you please tell me why this program has a syntax error with this 
> message
> "Recursive definiton ill-formed"? Maybe the syntax of recursive 
> function in Coq is not like
> ML etc?
>
> Thanks in advance.
>
> ------------------------
> Fixpoint oddmembers (l:natlist) : natlist :=
>   match l with
>     | nil =>nil
>     | h :: t =>
>       match h with
>         | 0 => oddmembers t
>         | 1 => 1 :: (oddmembers t)
>         | S (S h') =>  oddmembers (h' :: t)
>       end
>   end.
> --------------------

Your definition isn't obviously terminating; that is, the simple rule of 
primitive recursion doesn't show that it always terminates.  All Coq 
programs must terminate.  Therefore, to get Coq to accept your 
definition, you would have to use an explicit termination argument.

I believe this trouble is easy to avoid in your specific example, by 
using an auxiliary recursive function for deciding evenness.  (This 
would even lead to cleaner code that's easier to understand, which is 
not the usual case when someone hits a problem with termination 
checking. ;])