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 warningt 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
To check guards on all recursive calls:
To leave the current behavior unchanged except for inhibiting such messages: