The Coq mailing list

[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