Major Section: BREAK-REWRITE
Example Form: :ok-if (null (brr@ :wonp)) General Form: :ok-if exprwhere
expris a term involving no free variables other than
stateand returning one non-
stateresult which is treated as Boolean. This form is intended to be executed from within
Consider first the simple situation that the
(ok-if term) is a command
break-rewrite. Then, if the term is non-
break-rewrite exits and otherwise it does not.
ok-if returns an ACL2 error triple
(mv erp val state). (See ld or see programming-with-state for more on
error triples.) If any form being evaluated as a command by
break-rewrite returns the triple returned by
(ok-if term) then the
effect of that form is to exit break-rewrite if term is non-
Thus, one might define a function or macro that returns the value of
ok-if expressions on all outputs and thus create a convenient new way to
The exit test,
term, generally uses
brr@ to access context sensitive
information about the attempted rule application. See brr@.
useful inside of command sequences produced by break conditions.
:ok-if is most useful after an
:eval command has caused
break-rewrite to try to apply the rule because in the resulting break
expr can access such things as whether the rule succeeded, if
so, what term it produced, and if not, why. There is no need to use
:evaling the rule since the same effects could be
achieved with the break condition on the rule itself. Perhaps we should
replace this concept with
:eval-and-break-if? Time will tell.