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

[PVS-Help] symbol manipulation



I suspect this may be more to do with lisp than pvs,
so apologies if this is the wrong place for the question.

I have a defined strategy 'f' which takes as a formal parameter, 'name' 
(which is a predicate).  In addition to using 'name', I'd also like
to use the symbol formed by prepending "inv_" to 'name'. 
That is, if I invoke the strategy f with actual parameter "foo", I
also want to make use of the symbol "inv_foo".  

I can do this by adding a parameter to f and invoking f(foo,
inv_foo), but I'd prefer to just invoke f(foo), and internally to f
construct the symbol inv_foo.  Can I do this inside a strategy
definition?

Thanks,
Rob