coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Andrej Bauer <andrej.bauer AT andrej.com>
To: Daniel Schepler <dschepler AT gmail.com>
Cc: Victor Porton <porton AT narod.ru>, Coq <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Where is the set theory?
Date: Thu, 3 Nov 2011 22:10:16 +0100

> So yes, it's probably useless if you need things to be
> computable at the end. But if what you're doing is pure mathematical
> formalization, I don't see any drawbacks to using this construction.

Or you can be computable _and_ do pure mathematical formalization, to
get the best of both worlds.

With kind regards,

Andrej

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