The Coq mailing list

[muad <muad.dib.space AT gmail.com>]

Hello,

> Inductive test : Type :=
> | test1 : nat -> Type
> | test2 : nat -> nat -> Type

> 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
> the rest have "test2" as their constructor.

maybe it's not perfectly suitable but it might be possible to define it in
this way,

isTest1 : test -> Prop := ...
isTest2 : test -> Prop := fun s =>
 match s with test1 _ => False | test2 _ _ => True end.

Inductive plist (T : Type) (P : T -> Prop) (tail : Type) : Type :=
| pnil : tail -> plist T P tail
| pcons : forall t : T, P t -> plist T P tail -> plist T p tail.

then, plist test isTest1 (plist test isTest2 unit) holds that property.

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