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