		Search-engine friendly clone of the ACL2 documentation.

Expr-tools

Vl-exprlist-resolved-p

(vl-exprlist-resolved-p x) recognizes lists where every element satisfies vl-expr-resolved-p.

Signature
(vl-exprlist-resolved-p x) → std::bool

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

Definitions and Theorems

Function: vl-exprlist-resolved-p

(defun vl-exprlist-resolved-p (x)
       (declare (xargs :guard (vl-exprlist-p x)))
       (let ((__function__ 'vl-exprlist-resolved-p))
            (declare (ignorable __function__))
            (if (consp x)
                (and (vl-expr-resolved-p (car x))
                     (vl-exprlist-resolved-p (cdr x)))
                t)))

Subtopics

Vl-exprlist-resolved-p-basics: Basic theorems about vl-exprlist-resolved-p, generated by deflist.