		Search-engine friendly clone of the ACL2 documentation.

Logic-fns-listp

Recognizer for when a given list of terms calls only :logic-mode function symbols

For a list x of terms in world wrld, (logic-fns-listp x wrld) is true if and only if every function symbol called in x is in :logic mode in wrld. Unlike logic-term-listp, logic-fns-listp does not check that x is a list of terms; rather, logic-fns-listp should only be applied to such lists. See defun-mode-lambdas for some clarifications of how :program mode functions are allowed in certain :logic mode terms.

Function: logic-fns-listp

(defun logic-fns-listp (lst wrld)
  (declare (xargs :guard (and (plist-worldp wrld)
                              (pseudo-term-listp lst))))
  (cond ((endp lst) t)
        (t (and (logic-fnsp (car lst) wrld)
                (logic-fns-listp (cdr lst) wrld)))))