		Search-engine friendly clone of the ACL2 documentation.

Verilog-printing

Vl-ps-update-mimic-linebreaks

Set whether we should emulate linebreaks from the original input.

Signature
(vl-ps-update-mimic-linebreaks mimicp &key (ps 'ps)) → ps
Arguments: mimicp — Guard (booleanp mimicp).

We want the default to be t, so we look for disregard-linebreaks instead of mimic-linebreaks.

Definitions and Theorems

Function: vl-ps-update-mimic-linebreaks-fn

(defun vl-ps-update-mimic-linebreaks-fn (mimicp ps)
  (declare (xargs :stobjs (ps)))
  (declare (xargs :guard (booleanp mimicp)))
  (let ((__function__ 'vl-ps-update-mimic-linebreaks))
    (declare (ignorable __function__))
    (let* ((disregardp (not mimicp))
           (misc (vl-ps->misc))
           (misc (remove-from-alist :vl-disregard-linebreaks misc)))
      (vl-ps-update-misc (acons :vl-disregard-linebreaks
                                disregardp misc)))))

Theorem: vl-ps-update-mimic-linebreaks-fn-of-bool-fix-mimicp

(defthm vl-ps-update-mimic-linebreaks-fn-of-bool-fix-mimicp
  (equal (vl-ps-update-mimic-linebreaks-fn (acl2::bool-fix mimicp)
                                           ps)
         (vl-ps-update-mimic-linebreaks-fn mimicp ps)))

Theorem: vl-ps-update-mimic-linebreaks-fn-iff-congruence-on-mimicp

(defthm vl-ps-update-mimic-linebreaks-fn-iff-congruence-on-mimicp
  (implies
       (iff mimicp mimicp-equiv)
       (equal (vl-ps-update-mimic-linebreaks-fn mimicp ps)
              (vl-ps-update-mimic-linebreaks-fn mimicp-equiv ps)))
  :rule-classes :congruence)