The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Ruddy Hahn wrote:
> Inductive snatlist : Set :=
>   | snil : snatlist
>   | scons : forall (n : nat) (l : snatlist), ~ (occur n l) -> snatlist
> with occur (n : nat) (l : snatlist) : Prop :=
>   | ocHead : forall (n : nat) (l : snatlist) (p : ~ (occur n l)), 
> occur n (scons n l p)
>   | ocCons : forall (m  : nat) (l : snatlist) (p: ~ (occur n l)),
>       (occur m l) -> occur m (scons n l p)
>
> It does not work and yields error:
>  (Error: Parameters should be syntactically the same for each 
> inductive type.)

You want to be defining the inductive type indices as regular arguments, 
rather than parameters.  If you're not sure what I mean by this, then I 
think you'll find the answer in any introduction to Coq.

Even switching this won't help you.  When defining mutually inductive 
types, none of the types being defined may appear in the type of 
another.  Here you have [snatlist] appearing in the type of [occur], 
despite the fact that these types are mutually inductive.  You will need 
to use some less direct encoding to achieve what you're looking for.