[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