The Coq mailing list

[Charles Bouillaguet <Charles.Bouillaguet AT crans.org>]

Hi,

I think that what you want is :

Inductive A: Set :=
 | A1
 | A2 (x: B)

with B: Set :=
 | B1
 | B2 (x: A).

You may also want to define mutually recursive induction principle. You 
should probably read the section 10.3, about "Scheme" in the reference 
manual. You'll find some example there, too.

Good luck !

Charles Bouillaguet

Alex Suzuki wrote:
> Hello list,
>
> I'm a CS student at ETH Zurich and I'm using Coq to formalize a
> translation from Java Bytecode to a guarded command language used
> for verification. This is probably not the last question regarding
> Coq from my side. ;-)
>
> When a situation arises where we have types that depend on each
> other, how do you do write this in Coq?
>
> Inductive A: Set :=
>   | A1
>   | A2 (x: B).
>
> Inductive B: Set :=
>   | B1
>   | B2 (x: A).
>
> This will not work as Coq will complain that the reference B was
> not found in the current environment. Is there some way to
> "forward declare" type B, or am I doing something very wrong? :)
>
> Regards,
>   Alex