		Search-engine friendly clone of the ACL2 documentation.

Logic-term-listp

Recognizer for lists of terms that call only :logic-mode function symbols

This predicate strengthens (term-listp x wrld), as it also requires (logic-fns-listp x wrld), i.e., that every function symbol called in x is in :logic mode in the world, wrld.

Function: logic-term-listp

(defun logic-term-listp (x w)
  (declare (xargs :guard (plist-worldp-with-formals w)))
  (and (term-listp x w)
       (logic-fns-listp x w)))