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

[PVS-Help] Defining a strategy that takes a list as an argument and uses it with expand*



Hi all,

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)
  (then
   (apply 'expand* expand-list)
   (expand)
   (reveal reveal-name)
  )
  "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?

Best Regards,
Ben Hocking