The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Hello.

If you are only interested in finite sets, you can also try the FSet 
module. See the FSetUtil module of the CoLoR library to see how to use 
it. Definitions and lemmas without proofs can be seen on 
http://color.inria.fr/doc/CoLoR.Util.FSet.FSetUtil.html .

Regards,

Frédéric.

Le 25/04/2013 21:21, Vincent BENAYOUN a écrit :
> Hi everybody,
>
> I am using the Coq standard library for set.
> I consider :
> - Coq.Sets.Ensembles
> - Coq.Sets.Finite_sets
>
> How can I write a function which take a finite set and return a list 
> of its elements ?
> I have written the following code which obviously doesn't work.
> How can I fix it ?
>
>
> Require Import Ensembles.
> Require Import Finite_sets.
>
> Fixpoint finite_set_to_list (s:Ensemble label) (P:Finite _ s) : list 
> label :=
>   match P with
>     | Empty_is_finite => nil
>     | Union_is_finite s' P' x H => cons x (finite_set_to_list s' P')
>   end.
>
>
> Thanks in advance,
> Vincent