		Search-engine friendly clone of the ACL2 documentation.

Oddexpr-check

Vl-exprctxalist-oddexpr-check

Signature
(vl-exprctxalist-oddexpr-check x ss) → warnings
Arguments: x — Guard (vl-exprctxalist-p x).; ss — Guard (vl-scopestack-p ss).
Returns: warnings — Type (vl-warninglist-p warnings).

Definitions and Theorems

Function: vl-exprctxalist-oddexpr-check

(defun vl-exprctxalist-oddexpr-check (x ss)
  (declare (xargs :guard (and (vl-exprctxalist-p x)
                              (vl-scopestack-p ss))))
  (let ((__function__ 'vl-exprctxalist-oddexpr-check))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (append (vl-oddexpr-check (caar x) (cdar x) ss)
              (vl-exprctxalist-oddexpr-check (cdr x)
                                             ss)))))

Theorem: vl-warninglist-p-of-vl-exprctxalist-oddexpr-check

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