		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-states

Plexeme-list-not-tokenp

Check if no preprocessing lexeme in a list is a token.

Signature
(plexeme-list-not-tokenp x) → std::bool

This is an ordinary std::deflist. It is "loose" in that it does not care whether x is nil-terminated.

Definitions and Theorems

Function: plexeme-list-not-tokenp

(defun plexeme-list-not-tokenp (x)
  (declare (xargs :guard (plexeme-listp x)))
  (if (consp x)
      (and (not (plexeme-tokenp (car x)))
           (plexeme-list-not-tokenp (cdr x)))
    t))

Subtopics

Plexeme-list-not-tokenp-basics: Basic theorems about plexeme-list-not-tokenp, generated by std::deflist.