Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Check Record Field Membership in a List

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Check Record Field Membership in a List


chronological Thread 
  • From: CoqUser CoqUser <coquser AT yahoo.com>
  • To: coq-club AT pauillac.inria.fr
  • Subject: [Coq-Club] Check Record Field Membership in a List
  • Date: Wed, 29 Jul 2009 07:46:14 -0700 (PDT)
  • Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=s1024; d=yahoo.com; h=Message-ID:X-YMail-OSG:Received:X-Mailer:Date:From:Subject:To:MIME-Version:Content-Type; b=o8b5ObeM4oWdzO+6GfUACEIFnXgdhM6NNr4emQSrwcu1BDpLhzp6FGy1sMVCwya3WCdZrN6dSw260wV2pfoc+GbW/bEhhV6dcU5p+/MlLkTq17Gzq1YwMYo+eF1pR2lr5GioQWJyrxZ3JXG888SnIcbcIGnVbGeIbqWlT6eBDDw=;
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>


In the (very simplified) example below I want to check that all product's names appear in the list of product names in a Store.  However, I always get this error:
Error: In environment
p : Product
s : Store
The term "products s" has type "list Product"
while it is expected to have type "Product".

Any Ideas??

Example Code:
Require Import String.
Require Import List.
Record Product:Set := {productName:string}.
Record Store:Set := {products:list Product}.

Theorem T: forall p:Product,forall s:Store, In (productName p) (productName (products s)).
(*A product's name must be in the list of Product Names that a Store has.
How is this written?  I don't want to check that the Product is in the list of
Products, only that the name is in the Store's list of product names.*)








Archive powered by MhonArc 2.6.16.

Top of Page