		Search-engine friendly clone of the ACL2 documentation.

Verilog-printing

Vl-ps-update-copious-parens

Set whether we should print expressions with extra parentheses even where they are not needed.

Signature
(vl-ps-update-copious-parens copiousp &key (ps 'ps)) → ps
Arguments: copiousp — Guard (booleanp copiousp).

Definitions and Theorems

Function: vl-ps-update-copious-parens-fn

(defun vl-ps-update-copious-parens-fn (copiousp ps)
  (declare (xargs :stobjs (ps)))
  (declare (xargs :guard (booleanp copiousp)))
  (let ((__function__ 'vl-ps-update-copious-parens))
    (declare (ignorable __function__))
    (let* ((misc (vl-ps->misc))
           (misc (remove-from-alist :vl-copious-parens misc)))
      (vl-ps-update-misc (acons :vl-copious-parens (and copiousp t)
                                misc)))))

Theorem: vl-ps-update-copious-parens-fn-of-bool-fix-copiousp

(defthm vl-ps-update-copious-parens-fn-of-bool-fix-copiousp
  (equal (vl-ps-update-copious-parens-fn (acl2::bool-fix copiousp)
                                         ps)
         (vl-ps-update-copious-parens-fn copiousp ps)))

Theorem: vl-ps-update-copious-parens-fn-iff-congruence-on-copiousp

(defthm vl-ps-update-copious-parens-fn-iff-congruence-on-copiousp
  (implies
       (iff copiousp copiousp-equiv)
       (equal (vl-ps-update-copious-parens-fn copiousp ps)
              (vl-ps-update-copious-parens-fn copiousp-equiv ps)))
  :rule-classes :congruence)