		Search-engine friendly clone of the ACL2 documentation.

Guard-checking-inhibited

Avoiding certain warnings when evaluating ACL2 expressions

ACL2 sometimes omits the checking of guards on recursive calls of functions. This omission is signaled by a warning like the one shown below.

ACL2 !>(factorial 3)

ACL2 Warning [Guards] in TOP-LEVEL:  Guard-checking will be inhibited
for some recursive calls for FACTORIAL and perhaps other functions;
see :DOC guard-checking-inhibited.

6
ACL2 !>

This behavior can occur for a recursively-defined logic-mode function with a guard other than t whose guards have not been verified, when guard-checking has its default value, t. (Exceptions may occur, for example when the function is being traced.) No further such message is printed (for any function) before the next top-level form is submitted.

To check guards on all recursive calls:

(set-guard-checking :all)

To leave the current behavior unchanged except for inhibiting such messages:

(set-guard-checking :nowarn)