The Coq mailing list

[Jeff Terrell <jeff AT kc.com>]

Hi,

I'm trying to create functions to build types in which X references one or more 
Y, and Y references X.

In the case where X references one Y, the following function appears to work 
fine.

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

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

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.

Any help would be much appreciated.

Regards,
Jeff.