coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Chlipala <adamc AT csail.mit.edu>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Excluded Middle for Type?
- Date: Tue, 02 Jul 2013 15:40:48 -0400
Such an axiom certainly breaks extraction, since it has no natural computational interpretation, but perhaps you don't care about extraction. It also makes Gallina "computation" highly non-computational, which also might not bother you, depending on the application. I don't know if it's logically consistent.
On 07/02/2013 03:38 PM, Chris Casinghino wrote:
I notice that, where the Coq FAQ discusses safe axioms, it mentions
excluded middle only for "Prop". This also seems to be the case in
the standard libraries.
Would it also be safe to add excluded middle for "Type"? That is,
could I add the following?
Inductive sum (A B : Type) : Type :=
| leftT : A -> sum A B
| rightT : B -> sum A B.
Axiom em_type : forall A : Type, sum A (A -> False).
- [Coq-Club] Excluded Middle for Type?, Chris Casinghino, 07/02/2013
- Re: [Coq-Club] Excluded Middle for Type?, Adam Chlipala, 07/02/2013
- Re: [Coq-Club] Excluded Middle for Type?, Chris Casinghino, 07/02/2013
- Re: [Coq-Club] Excluded Middle for Type?, Viktor Vafeiadis, 07/02/2013
- Message not available
- Fwd: [Coq-Club] Excluded Middle for Type?, Jonas Kaiser, 07/02/2013
- Re: [Coq-Club] Excluded Middle for Type?, Chris Casinghino, 07/02/2013
- Fwd: [Coq-Club] Excluded Middle for Type?, Jonas Kaiser, 07/02/2013
- Re: [Coq-Club] Excluded Middle for Type?, Chris Casinghino, 07/02/2013
- Re: [Coq-Club] Excluded Middle for Type?, Adam Chlipala, 07/02/2013
- Re: [Coq-Club] Excluded Middle for Type?, Andrew Cave, 07/02/2013
Archive powered by MHonArc 2.6.18.