		Search-engine friendly clone of the ACL2 documentation.

Condcheck

Vl-exprctxalist-condcheck

(vl-exprctxalist-condcheck x) extends vl-expr-condcheck across an vl-exprctxalist-p.

Signature
(vl-exprctxalist-condcheck x) → warnings
Arguments: x — Guard (vl-exprctxalist-p x).
Returns: warnings — Type (vl-warninglist-p warnings).

Definitions and Theorems

Function: vl-exprctxalist-condcheck

(defun vl-exprctxalist-condcheck (x)
  (declare (xargs :guard (vl-exprctxalist-p x)))
  (let ((__function__ 'vl-exprctxalist-condcheck))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (append (vl-expr-condcheck (caar x)
                                 nil (cdar x))
              (vl-exprctxalist-condcheck (cdr x))))))

Theorem: vl-warninglist-p-of-vl-exprctxalist-condcheck

(defthm vl-warninglist-p-of-vl-exprctxalist-condcheck
  (b* ((warnings (vl-exprctxalist-condcheck x)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)