The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

On Mon, Mar 30, 2009 at 08:25:37AM -0700, dimitrisg7 wrote:
> 
> Hello!
> 
> I have the following inductive definition:
> 
> Inductive test : Type :=
> | test1 : nat -> Type
> | test2 : nat -> nat -> Type
> 
> and I want to define a data type, which is a list of "test" objects. Some
> first X items of that list have "test1" as their constructor and the rest
> have "test2" as their constructor. Is there a flexible way to define this? I
> would rather not break the inductive definition "test" into two pieces.

You will need to make it apparent in the type of 'test' which
constructor was applied; that is, you will need to make 'test' indexed.
For instance,

Inductive test : bool -> Type :=
  | test1 : nat -> Type true  
  | test2 : nat -> nat -> Type false
  .

(Untested, may have typos :) 

Edsko