The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hello Vincent, your definition is not accepted because Finite is a predicate in Prop. It is accepted with a version of Finite in Type instead. However if you describe what you want to do with them people in this list may suggest more pertinent definitions of finite sets.

Best regards,

P.

2013/4/25 Vincent BENAYOUN <benayoun.vincent AT gmail.com>

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