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

Re: [PVS-Help] Body of lemmas

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.