Set-verify-guards-eagerness
The eagerness with which guard verification is tried.
Example Forms: try guard verification?
(set-verify-guards-eagerness 0) ; no, unless :verify-guards t
(set-verify-guards-eagerness 1) ; yes if :guard, type or :stobjs is supplied
(set-verify-guards-eagerness 2) ; yes, unless :verify-guards nil
Note: This is an event! It does not print the usual event summary
but nevertheless changes the ACL2 logical world and is so recorded.
General Form:
(set-verify-guards-eagerness n)
where n is a variable-free term that evaluates to 0, 1, or
2. This macro is essentially equivalent to
(table acl2-defaults-table :verify-guards-eagerness n)
and hence is local to any books and encapsulate
events in which it occurs; see ACL2-defaults-table. However,
unlike the above simple call of the table event function (see table), no output results from a set-verify-guards-eagerness event.
Set-verify-guards-eagerness may be thought of as an event that merely
sets a flag to 0, 1, or 2. The flag is used by certain defun events to determine whether guard verification is tried.
The flag is irrelevant to those defun events in :program mode and to those defun events in which an explicit
:verify-guards setting is provided among the xargs. In
the former case, guard verification is not done because it can only be
done when logical functions are being defined. In the latter case, the
explicit :verify-guards setting determines whether guard
verification is tried. So consider a :logic mode defun
in which no :verify-guards setting is provided. Is guard
verification tried? The answer depends on the eagerness setting as follows.
If the eagerness is 0, guard verification is not tried. If the
eagerness is 1, it is tried if and only if a guard is explicitly
specified in the defun, in the following sense: there is an xargs
keyword :guard or :stobjs or a type declaration. If the
eagerness is 2, guard verification is tried.
The above remarks apply to verify-termination events,
according to whether guards are explicitly specified in the existing,
corresponding :program mode definitions.
The default behavior of the system is as though the
:verify-guards-eagerness is 1. The current behavior can be
ascertained by evaluating the form (default-verify-guards-eagerness (w
state)).
