The Coq mailing list

[dimitrisg7 <dvekris AT hotmail.com>]

Adam Koprowski wrote:
> 
>    Did you finish the proof with Defined instead of Qed? (the former will
> make the proof transparent, while the latter makes it opaque).
> 
> On Thu, Jul 16, 2009 at 10:21, Dimitris Vekris 
> <dvekris AT hotmail.com>
> wrote:
> 
>>  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<http://www.microsoft.com/windows/windowslive/>
>>
> 
> 
> 
> -- 
> =====================================================
> Adam.Koprowski AT gmail.com,
>  http://www.cs.ru.nl/~Adam.Koprowski
> The difference between impossible and possible
> lies in determination (Tommy Lasorda)
> =====================================================
> 
> 

This is the source of my problem and I was close to getting mad...
Thanks once again.


-----
Never say never.
-- 
View this message in context: 
http://www.nabble.com/%22function%22-is-opaque.-tp24512355p24512437.html
Sent from the Coq mailing list archive at Nabble.com.