		Search-engine friendly clone of the ACL2 documentation.

Chk-irrelevant-formals-ok

Check irrelevant-formals in definitions.

General Form:

 (chk-irrelevant-formals-ok def-or-defs)

where def-or-defs evaluates to a definition, a list of definitions, or a list of definitions preceded by mutual-recursion. Each definition must be a call of a macro in the following list: (defun defund defun-nx defund-nx defun$ defunt defun-inline defund-inline defun-notinline defund-notinline).

Example Forms:

; Success: Returns (value t).
(chk-irrelevant-formals-ok
 '(defun f (x0 x1 x2 x3 x4 x5)
    (declare (irrelevant x1 x3 x5 x4)
             (xargs :guard (natp x2)))
    (if (consp x0) (f (cdr x0) x1 x2 x5 x4 x3) nil)))

; Failure: Error message reports y irrelevant for both definitions.
(chk-irrelevant-formals-ok
 '(mutual-recursion
   (defun f1 (x y)
     (if (consp x) (f2 (cdr x) y) t))
   (defun f2 (x y)
     (if (consp x) (f1 (cdr x) y) nil))))

See irrelevant-formals-info for a related utility that returns a single value. By contrast, chk-irrelevant-formals-ok returns an error-triple, which is (mv nil t state) when the irrelevant-formals check passes for the given definition or list of definitions, and otherwise returns a soft error as in (er soft ...). Note that all relevant declare forms, including ``irrelevant'', are taken into account. For finer-grained control of the use of declarations, see irrelevant-formals-info.