		Search-engine friendly clone of the ACL2 documentation.

Logic-fnsp

Recognizer for when a given term calls only :logic-mode function symbols

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

Function: logic-fnsp

(defun logic-fnsp (term wrld)
  (declare (xargs :guard (and (plist-worldp wrld)
                              (pseudo-termp term))))
  (cond ((variablep term) t)
        ((fquotep term) t)
        ((flambdap (ffn-symb term))
         (and (logic-fnsp (lambda-body (ffn-symb term))
                          wrld)
              (logic-fns-listp (fargs term) wrld)))
        ((programp (ffn-symb term) wrld) nil)
        (t (logic-fns-listp (fargs term) wrld))))