coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.*)
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.*)
- [Coq-Club] Check Record Field Membership in a List, CoqUser CoqUser
- <Possible follow-ups>
- [Coq-Club] Check Record Field Membership in a List, CoqUser CoqUser
- Re: [Coq-Club] Check Record Field Membership in a List,
Adam Koprowski
- [Coq-Club] Canonical Structures Not at top level, Cedric Auger
- Re: [Coq-Club] Check Record Field Membership in a List,
Adam Koprowski
- [Coq-Club] Check Record Field Membership in a List,
Coq User
- Message not available
Archive powered by MhonArc 2.6.16.