		Search-engine friendly clone of the ACL2 documentation.

Server

Vls-data-origname-reportcard

Signature
(vls-data-origname-reportcard data) → reportcard
Arguments: data — Guard (vls-data-p data).
Returns: reportcard — Type (vl-reportcard-p reportcard).

Definitions and Theorems

Function: vls-data-origname-reportcard

(defun vls-data-origname-reportcard (data)
  (declare (xargs :guard (vls-data-p data)))
  (let ((__function__ 'vls-data-origname-reportcard))
    (declare (ignorable __function__))
    (b* (((vls-data data))
         (acc nil)
         (acc (vl-design-origname-reportcard-aux data.good acc))
         (acc (vl-design-origname-reportcard-aux data.bad acc))
         (ret (vl-clean-reportcard acc)))
      (fast-alist-free acc)
      ret)))

Theorem: vl-reportcard-p-of-vls-data-origname-reportcard

(defthm vl-reportcard-p-of-vls-data-origname-reportcard
  (b* ((reportcard (vls-data-origname-reportcard data)))
    (vl-reportcard-p reportcard))
  :rule-classes :rewrite)