coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Finite subsets of N in ssreflect?

From: Holden Lee <holdenlee AT alum.mit.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Finite subsets of N in ssreflect?
Date: Mon, 11 May 2015 22:28:44 -0400

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

[Coq-Club] Finite subsets of N in ssreflect?, Holden Lee, 05/12/2015
- Re: [Coq-Club] Finite subsets of N in ssreflect?, Laurent Théry, 05/12/2015
- Re: [Coq-Club] Finite subsets of N in ssreflect?, Matthieu Sozeau, 05/12/2015
  - Re: [Coq-Club] Finite subsets of N in ssreflect?, Pierre-Yves Strub, 05/12/2015
    - Re: [Coq-Club] Finite subsets of N in ssreflect?, Cyril Cohen, 05/13/2015
- Re: [Coq-Club] Finite subsets of N in ssreflect?, Frédéric Blanqui, 05/12/2015