coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Dominique Larchey-Wendling" <dominique.larchey-wendling AT loria.fr>
- To: <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] : is ∀A: Prop, ∼∼(A∨∼A) provable in Coq?
- Date: Thu, 03 Sep 2015 11:33:22 +0200
Le
3 septembre 2015 10:54:33 shengyu shen <shengyushen AT icloud.com> a
écrit :
Dear all:
I am trying to
prove an exercise in coq art “∀A: Prop,
∼∼(A∨∼A).”
I think this may need exclude
middle rule, which is not in “Calculus of
Inductive Constructions “
- [Coq-Club] : is ∀A: Prop, ∼∼(A∨∼A) provable in Coq?, shengyu shen, 09/03/2015
- Re: [Coq-Club] : is ∀A: Prop, ∼∼(A∨∼A) provable in Coq?, Pierre Casteran, 09/03/2015
- Re: [Coq-Club] : is ∀A: Prop, ∼∼(A∨∼A) provable in Coq?, Arnaud Spiwack, 09/03/2015
- Re: [Coq-Club] : is ∀A: Prop, ∼∼(A∨∼A) provable in Coq?, shengyu shen, 09/03/2015
- Re: [Coq-Club] : is ∀A: Prop, ∼∼(A∨∼A) provable in Coq?, Arnaud Spiwack, 09/03/2015
- Re: [Coq-Club] : is ∀A: Prop, ∼∼(A∨∼A) provable in Coq?, Dominique Larchey-Wendling, 09/03/2015
- Re: [Coq-Club] : is ∀A: Prop, ∼∼(A∨∼A) provable in Coq?, Pierre Casteran, 09/03/2015
Archive powered by MHonArc 2.6.18.