SET-VERIFY-GUARDS-EAGERNESS.html -- ACL2 Version 3.1

SET-VERIFY-GUARDS-EAGERNESS

the eagerness with which guard verification is tried.

Major Section:  EVENTS

Example Forms:                        try guard verification?
(set-verify-guards-eagerness 0) ; no, unless :verify-guards t
(set-verify-guards-eagerness 1) ; yes if a :guard 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 iff a :guard is explicitly provided in the defun. If the eagerness is 2, guard verification is tried.

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)).