The Coq mailing list

[Ruddy Hahn <ruddy.hahn AT gmail.com>]

Hello,

I am interested in representing lists of natural numbers without repetition of occurrences,

using inductive types.

Thus

 (1) The empty list is a list without repetition of occurrences.

 (2) If l is a list without repetition of occurrences, and if (n : nat) does not already

      occur in l, then (cons n l) is a list without repetition of occurrences

An attempt at defining snatlist as an inductive type is as follows:

(A snatlist is a list of natural numbers without repetition of occurrences.)

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.)

How could one fix that ?

Thanks a lot.

R.