		Search-engine friendly clone of the ACL2 documentation.

Stv2c-c-symbol-name

Stv2c-tailchars-p

(stv2c-tailchars-p x) recognizes lists where every element satisfies stv2c-tailchar-p.

Signature
(stv2c-tailchars-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: stv2c-tailchars-p

(defun stv2c-tailchars-p (x)
       (declare (xargs :guard (character-listp x)))
       (let ((__function__ 'stv2c-tailchars-p))
            (declare (ignorable __function__))
            (if (consp x)
                (and (stv2c-tailchar-p (car x))
                     (stv2c-tailchars-p (cdr x)))
                t)))

Subtopics

Stv2c-tailchars-p-basics: Basic theorems about stv2c-tailchars-p, generated by std::deflist.