coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Announcement: Finite set library with comprehension

From: "Strub, Pierre-Yves" <pierre-yves AT strub.nu>
To: coq-club AT inria.fr
Cc: coq-club-request AT inria.fr, Christian Doczkal <doczkal AT ps.uni-saarland.de>
Subject: Re: [Coq-Club] Announcement: Finite set library with comprehension
Date: Fri, 06 Feb 2015 14:57:39 +0100

On 2015-02-06 11:19, Christian Doczkal wrote:

Out of curiosity, what were the other two?

One of the two must be that one, that I wrote after the third time somebody asked me "How would you do finite sets over an infinite carrier in ssr". This is not something I'm planing to maintain anyway.

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

Regards,
-- Pierre-Yves.

Re: [Coq-Club] Announcement: Finite set library with comprehension, Christian Doczkal, 02/03/2015
- Re: [Coq-Club] Announcement: Finite set library with comprehension, Arnaud Spiwack, 02/05/2015
  - Re: [Coq-Club] Announcement: Finite set library with comprehension, Christian Doczkal, 02/06/2015
    - Re: [Coq-Club] Announcement: Finite set library with comprehension, Strub, Pierre-Yves, 02/06/2015
      - Re: [Coq-Club] Announcement: Finite set library with comprehension, Arnaud Spiwack, 02/09/2015
        
        Re: [Coq-Club] Announcement: Finite set library with comprehension, Cyril Cohen, 02/09/2015