coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Laurent Théry <Laurent.Thery AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Finite subsets of N in ssreflect?
Date: Tue, 12 May 2015 10:50:50 +0200

Could you work with {set 'I_n} for a well-choosen n?

On 05/12/2015 04:28 AM, Holden Lee wrote:

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