The Coq mailing list

[Matthew Brecknell <coq-club AT brecknell.org>]

On Sun, 2009-03-22 at 11:27 +0000, Jeff Terrell wrote:
> If A and B are mutually inductive types,
> 
> Inductive A : Set := Build_A : B -> A
> with B : Set := Build_B : A -> B
> 
> is it possible to construct terms a : A and b : B, so that a is constructed 
> with 
> b and b with a?

No. Allowing that would render the logic inconsistent. In fact, you can
prove that A is uninhabited:

Fixpoint A_empty (a: A) : False :=
  match a with
    | Build_A b =>
      match b with
        | Build_B a1 => A_empty a1
      end
  end.

See also Coq'Art section 6.6 (Empty types).

Depending on what you're trying to do, you might want to look into
coinductive types (Coq'Art chapter 13).

Cheers,
Matthew