The Coq mailing list

[Z <zell08v AT orange.fr>]

Hello everyone, 

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.
--------------------

Z.


-- 
Zhoulai FU

INRIA Rennes - Bretagne Atlantique
Campus Universitaire de Beaulieu
35042 RENNES Cedex - FRANCE