coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: roconnor AT theorem.ca
- To: Coq Club <coq-club AT pauillac.inria.fr>
- Subject: [Coq-Club] Why Opaque?
- Date: Thu, 8 Sep 2005 09:34:12 -0400 (EDT)
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
I've spent a little time reviewing some discussion about
Opaque/Transparency problems when dealing with well-founded recursion
<http://www.google.com/search?hl=en&lr=&q=+site%3Apauillac.inria.fr+coq+opaque&btnG=Search>
But I haven't figured out why anything is Opaque at all. In particular in
Coq 7.1 a change was made so that `` Constants declared as opaque (using
Qed) can no longer become transparent (a constant intended to be
alternatively opaque and transparent must be declared as transparent
(using Defined))''. There must have been a reason for this.
--
Russell O'Connor <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''
- [Coq-Club] Why Opaque?, roconnor
Archive powered by MhonArc 2.6.16.