coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Proof Irrelevance and Eta Conversion

From: muad <muad.dib.space AT gmail.com>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] Proof Irrelevance and Eta Conversion
Date: Sat, 17 Oct 2009 13:06:27 -0700 (PDT)
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hello,

is it possible to experiment with Proof Irrelevance and Eta in the
conversion rule?

I would like to write some proofs using this but axiomatizing seems to make
things extremely awkward because reduction is lost. Is there any nice way I
can test out my idea?

Thank you
--
View this message in context:
http://www.nabble.com/Proof-Irrelevance-and-Eta-Conversion-tp25941387p25941387.html
Sent from the Coq mailing list archive at Nabble.com.

[Coq-Club] Proof Irrelevance and Eta Conversion, muad
- Re: [Coq-Club] Proof Irrelevance and Eta Conversion, Hugo Herbelin