		Search-engine friendly clone of the ACL2 documentation.

Verilog-printing

Vl-ps-update-show-atts

Set whether Verilog-2005 (* key = val *)-style attributes should be displayed.

Signature
(vl-ps-update-show-atts showp &key (ps 'ps)) → ps
Arguments: showp — Guard (booleanp showp).

We want the default to be t, so we look for hide-atts instead of show-atts.

Definitions and Theorems

Function: vl-ps-update-show-atts-fn

(defun vl-ps-update-show-atts-fn (showp ps)
  (declare (xargs :stobjs (ps)))
  (declare (xargs :guard (booleanp showp)))
  (let ((__function__ 'vl-ps-update-show-atts))
    (declare (ignorable __function__))
    (let ((hidep (not showp))
          (misc (vl-ps->misc)))
      (vl-ps-update-misc (acons :vl-hide-atts hidep misc)))))

Theorem: vl-ps-update-show-atts-fn-of-bool-fix-showp

(defthm vl-ps-update-show-atts-fn-of-bool-fix-showp
  (equal (vl-ps-update-show-atts-fn (acl2::bool-fix showp)
                                    ps)
         (vl-ps-update-show-atts-fn showp ps)))

Theorem: vl-ps-update-show-atts-fn-iff-congruence-on-showp

(defthm vl-ps-update-show-atts-fn-iff-congruence-on-showp
  (implies (iff showp showp-equiv)
           (equal (vl-ps-update-show-atts-fn showp ps)
                  (vl-ps-update-show-atts-fn showp-equiv ps)))
  :rule-classes :congruence)