coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club]Mutually dependent types

From: Lionel Elie Mamane <lionel AT mamane.lu>
To: Alex Suzuki <as AT cynox.ch>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club]Mutually dependent types
Date: Tue, 6 Jun 2006 13:49:53 +0200
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Tue, Jun 06, 2006 at 11:54:52AM +0200, Alex Suzuki wrote:

> When a situation arises where we have types that depend on each
> other, how do you do write this in Coq?

These are mutually inductive types and get written as

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

--
Lionel

[Coq-Club]Mutually dependent types, Alex Suzuki
- Re: [Coq-Club]Mutually dependent types, Charles Bouillaguet
- Re: [Coq-Club]Mutually dependent types, Pierre Casteran
  - Re: [Coq-Club]Mutually dependent types, Alex Suzuki
- Re: [Coq-Club]Mutually dependent types, Lionel Elie Mamane