The Coq mailing list

[Alex Suzuki <as AT cynox.ch>]

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
--
Alex Suzuki | 
as AT cynox.ch
 | http://n.ethz.ch/student/asuzuki
Most people are other people. Their thoughts are someone else's
opinions, their lives a mimicry, their passions a quotation.
- Oscar Wilde