coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: [Coq-Club] Proof Irrelevance
- Date: Wed, 23 Oct 2013 02:09:05 +0300
Is it true that for all decidable Prop there is provable proof irrelevance?
If it's true, is there any general way how to make such proofs?
Also more specifically - how I can prove that
forall (n m:nat) (p1 p2: n<>m), p1 = p2 ?
forall (n m:nat) (p1 p2: n<>m), p1 = p2 ?
- [Coq-Club] Proof Irrelevance, Ilmārs Cīrulis, 10/23/2013
- Re: [Coq-Club] Proof Irrelevance, Jason Gross, 10/23/2013
- Re: [Coq-Club] Proof Irrelevance, Ilmārs Cīrulis, 10/23/2013
- Re: [Coq-Club] Proof Irrelevance, AUGER Cédric, 10/23/2013
- Re: [Coq-Club] Proof Irrelevance, Ilmārs Cīrulis, 10/23/2013
- Re: [Coq-Club] Proof Irrelevance, Robbert Krebbers, 10/23/2013
- Re: [Coq-Club] Proof Irrelevance, Jason Gross, 10/23/2013
Archive powered by MHonArc 2.6.18.