[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.
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:
<expressions to eval>
(error (condition) <error value>))