		Search-engine friendly clone of the ACL2 documentation.

Verilog-printing

Vl-pp-set-portnames

Signature
(vl-pp-set-portnames portdecls &key (ps 'ps)) → ps
Arguments: portdecls — Guard (vl-portdecllist-p portdecls).

Definitions and Theorems

Function: vl-pp-set-portnames-fn

(defun vl-pp-set-portnames-fn (portdecls ps)
  (declare (xargs :stobjs (ps)))
  (declare (xargs :guard (vl-portdecllist-p portdecls)))
  (let ((__function__ 'vl-pp-set-portnames))
    (declare (ignorable __function__))
    (b* ((names (vl-portdecllist->names portdecls))
         (misc (vl-ps->misc)))
      (vl-ps-update-misc (acons :portnames names misc)))))

Theorem: vl-pp-set-portnames-fn-of-vl-portdecllist-fix-portdecls

(defthm vl-pp-set-portnames-fn-of-vl-portdecllist-fix-portdecls
  (equal (vl-pp-set-portnames-fn (vl-portdecllist-fix portdecls)
                                 ps)
         (vl-pp-set-portnames-fn portdecls ps)))

Theorem: vl-pp-set-portnames-fn-vl-portdecllist-equiv-congruence-on-portdecls

(defthm
 vl-pp-set-portnames-fn-vl-portdecllist-equiv-congruence-on-portdecls
 (implies (vl-portdecllist-equiv portdecls portdecls-equiv)
          (equal (vl-pp-set-portnames-fn portdecls ps)
                 (vl-pp-set-portnames-fn portdecls-equiv ps)))
 :rule-classes :congruence)