The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Jeff Terrell wrote:
> However, in the case where X references many Y, I'm not sure how to 
> define the function.
>
> CoInductive X : Set :=
>    Build_X : nat -> list Y -> X
> with Y : Set :=
>    Build_Y : nat -> X -> Y.

This definition type-checks:

CoFixpoint Build_XY (n : nat) (m : nat) : X :=
  Build_X n (Build_YX m n :: nil)
with
  Build_YX (m : nat) (n : nat) : Y := Build_Y m (Build_XY n m).

...but I'm guessing that this isn't what you're looking for.  Can you 
explain what you are trying to do in your actual example?  Co-inductive 
types have many non-intuitive features, and it's quite possible that 
you'd be better off reformulating your development at a higher level.