Extrategies is a set of strategy combinators and Lisp functions for writting
strategies in PVS. Extrategies also contains improved versions of standard
PVS strategies for skolemizing, naming, labeling, replacing, splitting, etc.
Extrategies has been part of PVS since PVS 5.0 and is included in the latest release of PVS.
printf
, commentf
, now
, extrategies-about
deftactic
deforacle
unlabel*
, delabel
, relabel
, name-label
,
name-label*
, name-replace*
, discriminate
copy*
, protect
, with-focus-on
, with-focus-on@
mapstep
, mapstep@
, with-fresh-labels
, with-fresh-labels@
,
with-fresh-names
, with-fresh-names@
try@
, try-then
, try-then@
, finalize
, finalize*
, touch
,
for
, for@
, when
, when@
, unless
, unless@
, when-label
, when-label@
,
unless-label
, unless-label@
, if-label
, sklisp
skoletin
, skoletin*
, redlet
, redlet*
skeep
, skeep*
, skodef
, skodef*
, insteep
, insteep*
, unroll
tccs-expression
, tccs-formula
, tccs-formula*
, tccs-step
,
if-tcc-sequent
, with-tccs
eval-formula
, eval-formula*
, eval-expr
, eval
splash
, replaces
, rewrites
, rewrite*
, suffices
skip-steps
, show-debug-mode
, toggle-debug-mode