Re: [PVS-Help] Body of lemmas

[Erika Rice <erice@cs.washington.edu>]

On Fri, Jun 24, 2005 at 01:52:58PM -0400, Ben Di Vito wrote:
> 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.
> 

Can a lemma work when used as a rewrite rule but still not be visible?
For example, can it be the case that (rewrite "mylemma") works while
(lisp (show (formula-resolutions 'mylemma))) does not?

If so, how can I tell which lemmas are 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>))
> 
> 

Thanks for the tip.

    Erika