The Coq mailing list

[roconnor AT theorem.ca]

On Fri, 11 Aug 2006, David de Villiers wrote:

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

There are multiple represations of sets in Coq.  It is most common to 
represents sets as predicates.  You would represent this set as something 
like

Require Import Ensembles.

Definition X := Triple nat 1 2 3.

See <http://coq.inria.fr/library/Coq.Sets.Ensembles.html>.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''