		Search-engine friendly clone of the ACL2 documentation.

Vl-reportcard-revive-invalid-warnings

Vl-reportcard-revive-invalid-warnings-exec

Signature
(vl-reportcard-revive-invalid-warnings-exec x valid-fal nrev) → nrev
Arguments: x — Guard (vl-reportcard-p x).

Definitions and Theorems

Function: vl-reportcard-revive-invalid-warnings-exec

(defun vl-reportcard-revive-invalid-warnings-exec (x valid-fal nrev)
 (declare (xargs :stobjs (nrev)))
 (declare (xargs :guard (vl-reportcard-p x)))
 (declare (xargs :guard (hons-assoc-equal :design valid-fal)))
 (let ((__function__ 'vl-reportcard-revive-invalid-warnings-exec))
   (declare (ignorable __function__))
   (b*
     ((x (vl-reportcard-fix x))
      ((when (atom x)) (nrev-fix nrev))
      ((cons name1 warnings1) (car x))
      ((when (hons-get name1 valid-fal))
       (vl-reportcard-revive-invalid-warnings-exec (cdr x)
                                                   valid-fal nrev))
      (nrev (vl-revive-invalid-warnings-nrev name1 warnings1 nrev)))
     (vl-reportcard-revive-invalid-warnings-exec (cdr x)
                                                 valid-fal nrev))))

Theorem: vl-reportcard-revive-invalid-warnings-exec-of-vl-reportcard-fix-x

(defthm
  vl-reportcard-revive-invalid-warnings-exec-of-vl-reportcard-fix-x
 (equal
   (vl-reportcard-revive-invalid-warnings-exec (vl-reportcard-fix x)
                                               valid-fal nrev)
   (vl-reportcard-revive-invalid-warnings-exec x valid-fal nrev)))

Theorem: vl-reportcard-revive-invalid-warnings-exec-vl-reportcard-equiv-congruence-on-x

(defthm
 vl-reportcard-revive-invalid-warnings-exec-vl-reportcard-equiv-congruence-on-x
 (implies
  (vl-reportcard-equiv x x-equiv)
  (equal
       (vl-reportcard-revive-invalid-warnings-exec x valid-fal nrev)
       (vl-reportcard-revive-invalid-warnings-exec
            x-equiv valid-fal nrev)))
 :rule-classes :congruence)