		Search-engine friendly clone of the ACL2 documentation.

Delayredux

Vl-first-bad-gatearg-for-delayredux

For error reporting, find an arg that has a problem.

Signature
(vl-first-bad-gatearg-for-delayredux x) → *
Arguments: x — Guard (vl-plainarglist-p x).

Definitions and Theorems

Function: vl-first-bad-gatearg-for-delayredux

(defun vl-first-bad-gatearg-for-delayredux (x)
  (declare (xargs :guard (vl-plainarglist-p x)))
  (let ((__function__ 'vl-first-bad-gatearg-for-delayredux))
    (declare (ignorable __function__))
    (cond ((atom x) nil)
          ((vl-gatearg-ok-for-delayredux-p (car x))
           (vl-first-bad-gatearg-for-delayredux (cdr x)))
          (t (car x)))))

Theorem: vl-first-bad-gatearg-for-delayredux-under-iff

(defthm vl-first-bad-gatearg-for-delayredux-under-iff
  (implies (force (vl-plainarglist-p x))
           (iff (vl-first-bad-gatearg-for-delayredux x)
                (not (vl-gateargs-ok-for-delayredux-p x)))))

Theorem: vl-plainarg-p-of-vl-first-bad-gatearg-for-delayredux

(defthm vl-plainarg-p-of-vl-first-bad-gatearg-for-delayredux
 (implies
      (force (vl-plainarglist-p x))
      (equal (vl-plainarg-p (vl-first-bad-gatearg-for-delayredux x))
             (not (vl-gateargs-ok-for-delayredux-p x)))))