Do a list of 4v-sexprs always evaluate to purely Boolean values, i.e., are they never X or Z?
(4v-sexpr-purebool-list-p x) → std::bool
This is a logically nice, but non-executable way to express pure Boolean-ness. See also 4v-sexpr-purebool-list-check, which can be executed; it uses a SAT solver to answer the question.
(defun 4v-sexpr-purebool-list-p (x) (declare (xargs :guard t)) (let ((__function__ '4v-sexpr-purebool-list-p)) (declare (ignorable __function__)) (if (consp x) (and (4v-sexpr-purebool-p (car x)) (4v-sexpr-purebool-list-p (cdr x))) t)))