The Coq mailing list

[Lionel Elie Mamane <lionel AT mamane.lu>]

On Fri, Aug 11, 2006 at 04:20:38PM -0400, 
roconnor AT theorem.ca
 wrote:

>> I am a newcomer to Coq and would like to know how to define
>> sets of the form
>> X={1,2,3}.

> There are multiple represations of sets in Coq.  It is most common
> to represents sets as predicates.

Alternatively, for finite sets, a list/heap/... can be adequate is
some cases. (If you use lists, you'll want to use another equality
than the Coq equality as your main interesting equality.)

-- 
Lionel