		Search-engine friendly clone of the ACL2 documentation.

4v-sexpr-purebool-p

4v-sexpr-purebool-list-p

Do a list of 4v-sexprs always evaluate to purely Boolean values, i.e., are they never X or Z?

Signature
(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.

Definitions and Theorems

Function: 4v-sexpr-purebool-list-p

(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)))

Subtopics

4v-sexpr-purebool-list-p-basics: Basic theorems about 4v-sexpr-purebool-list-p, generated by std::deflist.