The Coq mailing list

["Pierre Cast�ran" <pierre.casteran AT labri.fr>]

Hi,


May I assume you meant :

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


In this case, is the following solution Ok, or did you mean something
else ?
Pierre


Require Import List.

Definition tests := list test.


Inductive Ok2 : tests -> Prop :=
 Ok2_nil : Ok2 nil
|Ok2_cons : forall i j l, Ok2 l -> Ok2 (test2 i j::l).

Inductive Ok : tests -> Prop :=
 Ok_nil : forall l, Ok2 l -> Ok l
|Ok_cons : forall i  l, Ok l -> Ok (test1 i ::l).


Definition Tests := {l : tests | Ok l}.



Quoting 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.
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club



Pierre Castéran