(vl-exprctxalist-leftright-check x) extends vl-expr-leftright-check across an vl-exprctxalist-p.
(vl-exprctxalist-leftright-check x) → warnings
Function:
(defun vl-exprctxalist-leftright-check (x) (declare (xargs :guard (vl-exprctxalist-p x))) (let ((__function__ 'vl-exprctxalist-leftright-check)) (declare (ignorable __function__)) (b* (((when (atom x)) nil) ((cons expr ctx) (car x)) (indexy (vl-expr-indexy-via-ctx expr ctx))) (append (vl-expr-leftright-check expr indexy ctx) (vl-exprctxalist-leftright-check (cdr x))))))
Theorem:
(defthm vl-warninglist-p-of-vl-exprctxalist-leftright-check (b* ((warnings (vl-exprctxalist-leftright-check x))) (vl-warninglist-p warnings)) :rule-classes :rewrite)