The Coq mailing list

[Pierre-Yves Strub <pierre-yves AT strub.nu>]

Hi,

You could start with that:

  https://github.com/strub/ssrmisc/blob/master/fset.v

while waiting for Cyril to release its library (Yes, Cyril, I putting a bit of pressure on you -- we are all waiting :) )

Best,

-- Pierre-Yves.

2015-05-12 10:55 GMT+02:00 Matthieu Sozeau <mattam AT mattam.org>:

Hi Holden,

I know Cyril Cohen is developing such a library and I believe it will be part of the next release of mathcomp, maybe you can get in touch with him. There is no way to do that today otherwise AFAIK (if it's unbounded). There are of course FSets from the stdlib too which you can use.
Best,
-- Matthieu

Le mar. 12 mai 2015 à 04:29, Holden Lee <holdenlee AT alum.mit.edu> a écrit :

Hi,

I'd like to build on ssreflect for my development because it has an extensive library on finite sets. However, finset requires a finite type. How could I work with finite subsets of the natural numbers in ssreflect?

Thanks,

Holden