coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Where is the set theory?

From: Adam Chlipala <adamc AT csail.mit.edu>
To: Daniel Schepler <dschepler AT gmail.com>
Cc: Coq <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Where is the set theory?
Date: Thu, 03 Nov 2011 17:32:23 -0400

Daniel Schepler wrote:

Or, if you don't care about computability, prove the uniqueness of suprema, and then use constructive_definite_description (from the Description module) to build a function

Oh, I see. The same name is used in [ConstructiveEpsilon]. Confusing. :)

Re: [Coq-Club] Where is the set theory?, (continued)