coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Alternate proof that classic -> proof_irrelevance

From: Andrej Bauer <(e29315a54f%hidden_head%e29315a54f)andrej.bauer(e29315a54f%hidden_at%e29315a54f)andrej.com(e29315a54f%hidden_end%e29315a54f)>
To: Daniel Schepler <(e29315a54f%hidden_head%e29315a54f)dschepler(e29315a54f%hidden_at%e29315a54f)gmail.com(e29315a54f%hidden_end%e29315a54f)>
Cc: Coq Club <(e29315a54f%hidden_head%e29315a54f)coq-club(e29315a54f%hidden_at%e29315a54f)inria.fr(e29315a54f%hidden_end%e29315a54f)>
Subject: Re: [Coq-Club] Alternate proof that classic -> proof_irrelevance
Date: Mon, 14 May 2012 00:24:15 +0200

This is nice, but may I suggest that you don't call your proposition
"bool" and its two proofs "false" and "true". That's horribly
misleading.

With kind regards,

Andrej

[Coq-Club] Alternate proof that classic -> proof_irrelevance, Daniel Schepler, 05/10/2012
- Re: [Coq-Club] Alternate proof that classic -> proof_irrelevance, Andrej Bauer, 05/14/2012