coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- [Coq-Club]Seeking help on Coq, Israt Jahan
- Re: [Coq-Club]Seeking help on Coq, Pierre Casteran
- <Possible follow-ups>
- [Coq-Club]Seeking help on Coq,
Israt Jahan
- Re: [Coq-Club]Seeking help on Coq, Adam Chlipala
Archive powered by MhonArc 2.6.16.