coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] is there a [Type] for which it is unprovable in coq if it is empty or not?

From: Georgi Guninski <guninski AT guninski.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] is there a [Type] for which it is unprovable in coq if it is empty or not?
Date: Thu, 26 May 2011 20:16:09 +0300
Header: best read with a sniffer

please excuse my dumbness.

is there a [Type] for which it is unprovable in coq if it is empty or not?

is it possible to define a [Type] in coq for which no one can prove in coq if
it is empty or not?

related is: is it possible to define a Prop in coq for which no one can prove
in coq if it is True or False?

[Coq-Club] is there a [Type] for which it is unprovable in coq if it is empty or not?, Georgi Guninski
- Re: [Coq-Club] is there a [Type] for which it is unprovable in coq if it is empty or not?, AUGER Cedric
- Re: [Coq-Club] is there a [Type] for which it is unprovable in coq if it is empty or not?, Daniel Schepler
- <Possible follow-ups>
- Re: [Coq-Club] is there a [Type] for which it is unprovable in coq if it is empty or not?, Thierry Martinez