I’m trying to better understand how to create more complex strategies in PVS. To that end, I have the following strategy:
(defstep expand-grind-reveal (expand-list reveal-name)
(apply 'expand* expand-list)
"Expands, grinds, and reveals"
"Expanding '~a', grinding, and revealing")
However, when I run this, the expand* strategy is definitely not running. If I try the apply step by itself:
(apply 'expand* (“function_a” “function_b” “function_b2”))
I get the following result:
Ill-formed rule/strategy: expand*
Can anyone give me advice on what I might be doing wrong?