coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club]problems with listSet

From: "Mateus Oliveira" <mateus.oliveira AT gmail.com>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club]problems with listSet
Date: Sat, 18 Nov 2006 22:00:29 +0100
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:message-id:date:from:to:subject:mime-version:content-type:content-transfer-encoding:content-disposition; b=gYYg3slVYLNoObL1hHX6NbOO8KSrccRh+JNYM41TYZCzl18XG9JGVgiwVDGh1swYsoEIqPg8JKZLlUnIyKgg9qiH1uqrMGvPwC7RAAMywhzyobBw0JPpZ8qkS9ysiPI5YvyWzv54aTbTFOHmClsu1roBgXnzjXyvn0T0XIdN7dE=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

I'm having problems with the use of functions defined in
the ListSet library. For example, the following definition
causes an error:

Require Export ListSet.
Definition test_union(l1 l2:set nat):set nat:= set_union l1 l2.

Error: In environment
l1: set nat
l2: set nat
The term "l1" has type "set nat" while it is expected to have type
"forall x y : ?1, {x=y} + {x<>y}"

I don't understand why l1 must not have type "set nat" in this example.
What should I do to make this simple definition be accepted?

Thanks for any help,

mateus

[Coq-Club]problems with listSet, Mateus Oliveira
- Re: [Coq-Club]problems with listSet, Adam Chlipala
- [Coq-Club]Re: problems with listSet, Mateus Oliveira