coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Frédéric Blanqui <frederic.blanqui AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Finite subsets of N in ssreflect?
Date: Tue, 12 May 2015 17:05:29 +0200

Hello. The CoLoR library provides a few files on (finite) subsets of elements of an arbitrary type. See SetUtil.v and FinSet.v. Best regards, Frédéric.

Le 12/05/2015 04:28, Holden Lee 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

[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