The Coq mailing list

[Jeff Terrell <jeff AT kc.com>]

Hi,

Is Coq being too conservative in rejecting the definition of f?

Require Import List.

CoInductive A : Set :=
  Build_A : list B -> A
with B : Set :=
  Build_B : A -> B.

Definition RB := fun a : A => let (RB) := a in RB.
Definition RA := fun b : B => let (RA) := b in RA.

CoInductive X : Set :=
  Build_X : list Y -> X
with Y : Set :=
  Build_Y : X -> Y.

CoFixpoint f(a : A) : X :=
  Build_X (map g (RB a))
with g (b : B) : Y :=
   Build_Y (f (RA b)).

Thanks.

Regards,
Jeff.