The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

Israt Jahan wrote:

> Inductive known_in : C -> SD -> Prop :=
> E0 : (c1 c2 : C) (s :SD) (known_in c1 s) -> (known_in c1 (cons C c2 s))
>  
> Here, I have  declared C as Set, SD is defined as (list C). While  
> compiling this line in Coq, it declares that c2 is defined as type C 
> but it must be of type listSet.

The first argument of 'cons' is an implicit argument.  Simply leave it 
out and your example should work fine.

Israt Jahan wrote:

>      When I write ' Require Import securite', then after compilation, 
> the answer is securite library is not found on the load path. Sir, my 
> question is whether securite library exists in coq version 8.0.

I've never heard of that library.  You can check what's in the standard 
library here:
   http://coq.inria.fr/library-eng.html

As a meta-point, I suggest giving future messages to this mailing list 
more descriptive titles, related to the actual problems you are facing.