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

Re: Question on writing a strategy




Tamarah:
 
 >  (defstep my_strat (&optional min max (fnum +))
 >     (if (< min max) (then (inst-cp fnum min)(my_strat$ (+ min 1) max fnum))
 >		       (then (if (eq min max) (inst fnum min)(skip))))
 >       "instantiate fnum with all values from min to max"
 >       "instantiate fnum with all values from min to max"
 >  )

Lisp expressions such as (+ min 1) can not be arbitrarily mixed
with strategy expressions. In the strategy above it is required
to use a LET binding (similar to LET* in Lisp)

     ...
     (let ((minsucc (+ min 1)))
       ...
               ... (my_strat$ minsucc max fnum) ...)

For a description of the LET basic strategy see section 5.6.4 on
page 108 of the PVS prover manual.

Hope this helps,

Harald