The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT pps.jussieu.fr>]

On Wed, Jul 21, 2010 at 06:35:51PM +0100, David Pereira wrote:
> Hi all,
> 
> Does anyone know about any implementation of the powerset
> construction for finite sets that is compatible with the FSet
> library of Coq's standard library?
> 

Hi,

I've seen you've already had a couple of answers to your question
while I was on holidays, But if you're still interested, here is
another one: I made some time ago a few experiments and proofs in a
file named ... PowerSet.v in the user's contribution Orsay/FSets
(where can also be found btw old versions and various other stuffs
concerning FSets/FMaps). The file can be browsed online here:

https://gforge.inria.fr/scm/viewvc.php/*checkout*/trunk/Orsay/FSets/PowerSet.v?root=coq-contribs

Best regards,

Pierre