coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Interest in Coq-based mathematics classes?

From: Andrej Bauer <andrej.bauer AT andrej.com>
To: Daniel Schepler <dschepler AT gmail.com>
Cc: Coq Club <coq-club AT inria.fr>, Adam Chlipala <adamc AT csail.mit.edu>
Subject: Re: [Coq-Club] Interest in Coq-based mathematics classes?
Date: Thu, 27 Sep 2012 23:03:21 -0400

Finite combinatorics happens in the world of finite sets with
decidable equality. So I would suggest that throghout you work with
such sets. They are closed under many operations, and it would make
sense to build a library for them.

Or you could go all fancy and implement combinatorial species.

With kind regards,

Andrej

Re: [Coq-Club] Interest in Coq-based mathematics classes?, (continued)