		Search-engine friendly clone of the ACL2 documentation.

Use-set

Vl-mark-wires-for-arguments

Signature
(vl-mark-wires-for-arguments x alist) → (mv new-alist warning-wires)
Arguments: x — Guard (vl-arguments-p x).; alist — Guard (vl-wireinfo-alistp alist).
Returns: new-alist — Type (vl-wireinfo-alistp new-alist), given the guard.; warning-wires — Type (string-listp warning-wires), given the guard.

Definitions and Theorems

Function: vl-mark-wires-for-arguments

(defun vl-mark-wires-for-arguments (x alist)
  (declare (xargs :guard (and (vl-arguments-p x)
                              (vl-wireinfo-alistp alist))))
  (let ((__function__ 'vl-mark-wires-for-arguments))
    (declare (ignorable __function__))
    (vl-arguments-case
         x
         :vl-arguments-named
         (mv alist
             (vl-exprlist-names (vl-namedarglist-allexprs x.args)))
         :vl-arguments-plain
         (vl-mark-wires-for-plainarglist x.args alist nil))))

Theorem: vl-wireinfo-alistp-of-vl-mark-wires-for-arguments.new-alist

(defthm vl-wireinfo-alistp-of-vl-mark-wires-for-arguments.new-alist
  (implies (and (force (vl-arguments-p x))
                (force (vl-wireinfo-alistp alist)))
           (b* (((mv ?new-alist ?warning-wires)
                 (vl-mark-wires-for-arguments x alist)))
             (vl-wireinfo-alistp new-alist)))
  :rule-classes :rewrite)

Theorem: string-listp-of-vl-mark-wires-for-arguments.warning-wires

(defthm string-listp-of-vl-mark-wires-for-arguments.warning-wires
  (implies (and (force (vl-arguments-p x))
                (force (vl-wireinfo-alistp alist)))
           (b* (((mv ?new-alist ?warning-wires)
                 (vl-mark-wires-for-arguments x alist)))
             (string-listp warning-wires)))
  :rule-classes :rewrite)