[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, Erika Rice 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

Apparently the problem is that lemma names are case sensitive but the
quoted name is always converted to lower case.  Thus, the problem was
that I had a lemma myLemma and 
      (lisp (show (formula-resolutions 'myLemma)))
would be converted to 
      (lisp (show (formula-resolutions 'mylemma)))
which does not match myLemma.