coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] proof_irrelevance question

From: Stéphane Glondu <steph AT glondu.net>
To: "Samuel E. Moelius III" <moelius AT cis.udel.edu>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] proof_irrelevance question
Date: Sat, 01 Nov 2008 20:17:59 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Openpgp: id=FCE03DAA

Samuel E. Moelius III wrote:
> In the following example, is use of proof_irrelevance necessary? Is
> there some way to avoid its use when the domain of the predicate
> involved is nat, for example?

In that particular case, there might be. See the "Proof irrelevance for
le" thread in the archives of this mailing-list.

Cheers,

--
Stéphane

[Coq-Club] proof_irrelevance question, Samuel E. Moelius III
- Re: [Coq-Club] proof_irrelevance question, Stéphane Glondu
  - Re: [Coq-Club] proof_irrelevance question, Stéphane Glondu