The Coq mailing list

[Jesse Clayton <j89clayton89 AT gmail.com>]

Hi,

I wish to define function f1:

Require Import List.

Variable exp: forall (T: list nat), Type -> Type -> Type.

Variable b c: Type.

Fixpoint f1 (T: list nat):  Type:=

match T with

  | nil => exp nil b c

  | _::T2 => 

      exp T2 (f1 T2) (f2 T2) 

  end

with f2 (T: list nat): Type:=

match T with

  | nil => exp nil b c

  | n::T2 => 

      exp T2 (f1 T) (f2 T2) 

end.

but Coq returns "Recursive of f2 is ll-formed.". Do you have any idea how to solve this?

Thanks a lot.