coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Luke Palmer <lrpalmer 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 00:25:18 -0800
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; b=v+WMTNW04HVYBH9C5a8xJ9dBp95Be5vXPL8lOwdA/DEDg5801m5MbNWgAmSCGx0pV3 DHdF9fyvKOSV+L6Kx3i8EaccOXSELnB1nTCWEdrjSThCHwlkzUKlwx8yd0opoDpPU43p 1UglnRh9ESAn52A6Jc4J2sozAThShJO6k/W4c=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Thu, Jul 16, 2009 at 12:21 AM, 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.

unfold replaces a symbol by its definition. �But here f is abstract; it has no definition. �What are you expecting this to do?

Luke

[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