		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-states

Plexeme-list-token/newline-p

Check if every preprocessing lexeme in a list is a token or newline.

Signature
(plexeme-list-token/newline-p 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-token/newline-p

(defun plexeme-list-token/newline-p (x)
  (declare (xargs :guard (plexeme-listp x)))
  (if (consp x)
      (and (plexeme-token/newline-p (car x))
           (plexeme-list-token/newline-p (cdr x)))
    t))

Subtopics

Plexeme-list-token/newline-p-basics: Basic theorems about plexeme-list-token/newline-p, generated by std::deflist.