coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] "function" is opaque.

From: Adam Koprowski <adam.koprowski AT gmail.com>
To: Dimitris Vekris <dvekris AT hotmail.com>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] "function" is opaque.
Date: Thu, 16 Jul 2009 10:24:54 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; b=dSIgxVs95SX46R0FFtmqqT4dw4MFvOpsO+EiBoSXKApdDmYKhZwq8hze0hdpXj90dX sdGftDAOOwAyQNcgQXzmX+W5WIU2JUrj0W3ttKpXVg1VLXEwrZqL6rlNvzJK+VW82Wt8 SHcyCx85Gj9PTEseQve/8tB6UFQBSTTy2AwWs=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

�� 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

--
=====================================================
Adam.Koprowski AT gmail.com, http://www.cs.ru.nl/~Adam.Koprowski
The difference between impossible and possible
lies in determination (Tommy Lasorda)
=====================================================

[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