coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Dimitris Vekris <dvekris AT hotmail.com>
- To: <coq-club AT pauillac.inria.fr>
- Subject: [Coq-Club] "function" is opaque.
- Date: Thu, 16 Jul 2009 11:21:02 +0300
- Importance: Normal
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hello everyone. I am trying to unfold a function that I have written in 'proof mode' and I am getting this error. I know that you get this when for example you have: Variable f: A -> B. Theorem bla_bla. ... unfold f. But this is not my case. What may be the reasons for this kind of error? Thanks! Dimitris check out the rest of the Windows Live™. More than mail–Windows Live™ goes way beyond your inbox. More than messages |
- [Coq-Club] "function" is opaque., Dimitris Vekris
- Re: [Coq-Club] "function" is opaque.,
Adam Koprowski
- Re: [Coq-Club] "function" is opaque., dimitrisg7
- Re: [Coq-Club] "function" is opaque.,
Luke Palmer
- Re: [Coq-Club] "function" is opaque., Luke Palmer
- Re: [Coq-Club] "function" is opaque.,
Adam Koprowski
Archive powered by MhonArc 2.6.16.