		Search-engine friendly clone of the ACL2 documentation.

Use-set

Vl-mark-wires-used

Signature
(vl-mark-wires-used x warnp alist) → new-alist
Arguments: x — Guard (string-listp x).; alist — Guard (vl-wireinfo-alistp alist).
Returns: new-alist — Type (vl-wireinfo-alistp new-alist), given the guard.

Definitions and Theorems

Function: vl-mark-wires-used

(defun vl-mark-wires-used (x warnp alist)
  (declare (xargs :guard (and (string-listp x)
                              (vl-wireinfo-alistp alist))))
  (let ((__function__ 'vl-mark-wires-used))
    (declare (ignorable __function__))
    (if (atom x)
        alist
      (let ((alist (vl-mark-wire-used (car x)
                                      warnp alist)))
        (vl-mark-wires-used (cdr x)
                            warnp alist)))))

Theorem: vl-wireinfo-alistp-of-vl-mark-wires-used

(defthm vl-wireinfo-alistp-of-vl-mark-wires-used
  (implies (and (force (string-listp x))
                (force (vl-wireinfo-alistp alist)))
           (b* ((new-alist (vl-mark-wires-used x warnp alist)))
             (vl-wireinfo-alistp new-alist)))
  :rule-classes :rewrite)