Ssreflect Users Discussion List

[Christian Doczkal <>]

Hello

> More specifically, you should use the Choice interface, because it is
> more directly suited to your purposes, and is more general and more
> widely available than the Countable interface 

> there’s a little theory of that developed by Cyril Cohen in quotient.v
> (but this is still experimental work-in-progress).

Is this available somewhere

> In your case this would amount to representing finite sets with
> something like
> 
>       Record { elems : seq T ; _ : uniq elems; elems == choose (perm_eq 
> elems) elems }
> 
> with T : choiceType.

Unfortunately?, I already had developed the theory up to the powerset
construction using sorted/contType. I just tried to port this to
choiceType wich worked nicely except for the definition of powerset.

My definition of powerset uses recursion on the sorted list and
therefore relies on the fact that the representation invariant is
preserved unter behead.

So how could one go about defining the powerset with this
representation.

-- 
Regards
Christian