[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS-Help] Body of lemmas



On Friday 24 June 2005 13:22, you wrote:
> When I  try
>     Rule? (lisp (show (formula-resolutions 'mylemma)))
> I get the error
>     Error: No methods applicable for generic function
>            #<standard-generic-function actuals> with args
>            (mylemma) of classes (symbol)
>       [condition type: program-error]
>
> I am using PVS 3.2.  Any enlightenment would be appreciated.
>
>        Erika

Hmm.  It looks like mylemma is not visible in this context.  As far as failing 
with an unhandled exception like that, Sam Owre would have to decide if 
that's an issue.  There might be assumptions about function 
formula-resolutions and how it's called, e.g., that it should only be called 
with a name known to be valid.

As far as I know, this operation should work if the lemma name is visible to 
the formula whose proof you're working on.  If you're trying to reference a 
lemma whose theory hasn't been imported or a lemma that appears later in the 
same theory as the formula under proof, then it won't be visible.

By the way, you can protect yourself from Lisp exceptions using a wrapper such 
as the following:

  (handler-case
    <expressions to eval>
    (error (condition) <error value>))


Ben