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

[PVS-Help] args1 and strategies

I am trying to write a strategy and want to extract the argument of a
formula using args1.  The relevant bit of the strategy looks like

    (if (forall-expr? form) 
        (let ((form1 (args1 form))) 

When I try to run the strategy, I get the following error:

    Error: No methods applicable for generic function
           #<standard-generic-function args1> with args
           ((FORALL (sigma):
           of classes (forall-expr)

Am I using args1 incorrectly?  Do I need to load something special to
use it?  If so, what?

Thank you,

    Erika Rice