Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club]Seeking help on Coq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club]Seeking help on Coq


chronological Thread 
  • From: Adam Chlipala <adamc AT cs.berkeley.edu>
  • To: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club]Seeking help on Coq
  • Date: Thu, 23 Mar 2006 08:49:31 -0800
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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.





Archive powered by MhonArc 2.6.16.

Top of Page