coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club]Re: problems with listSet

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

David Pichardie wrote.

If you define :
Require Export ListSet.
Require Export Arith.

Definition union : set nat -> set nat -> set nat := set_union eq_nat_dec.

it works fine.

So, It works fine.

thanks,

mateus

2006/11/18, Mateus Oliveira
<mateus.oliveira AT gmail.com>:

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