The Coq mailing list

[dimitrisg7 <dvekris AT hotmail.com>]

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.

Thanks everyone!
-- 
View this message in context: 
http://www.nabble.com/Defining-data-types.-tp22785725p22785725.html
Sent from the Coq mailing list archive at Nabble.com.