		Search-engine friendly clone of the ACL2 documentation.

Vl-println

Vl-println-main

Signature
(vl-println-main x &key (ps 'ps)) → ps
Arguments: x — Guard (vl-printable-p x).

Definitions and Theorems

Function: vl-println-main-fn

(defun
 vl-println-main-fn (x ps)
 (declare (xargs :stobjs (ps)))
 (declare (xargs :guard (vl-printable-p x)))
 (let
  ((__function__ 'vl-println-main))
  (declare (ignorable __function__))
  (let*
   ((rchars (vl-ps->rchars))
    (col (vl-ps->col))
    (htmlp (vl-ps->htmlp))
    (x (vl-printable-fix x))
    (x (cond ((stringp x) x)
             ((and (atom x) x) (explode-atom x 10))
             (t x))))
   (declare (type (integer 0 *) col))
   (if
    htmlp
    (b*
     ((tabsize (vl-ps->tabsize))
      ((mv & rchars)
       (if (stringp x)
           (str::html-encode-string-aux x 0 (length x)
                                        col tabsize rchars)
           (str::html-encode-chars-aux x col tabsize rchars))))
     (vl-ps-seq
        (vl-ps-update-rchars (revappend (str::html-newline) rchars))
        (vl-ps-update-col 0)))
    (if
     (stringp x)
     (vl-ps-seq
          (vl-ps-update-rchars (cons #\Newline (cons x rchars)))
          (vl-ps-update-col 0))
     (vl-ps-seq
         (vl-ps-update-rchars (cons #\Newline (revappend x rchars)))
         (vl-ps-update-col 0)))))))

Theorem: vl-println-main-fn-of-vl-printable-fix-x

(defthm vl-println-main-fn-of-vl-printable-fix-x
        (equal (vl-println-main-fn (vl-printable-fix x)
                                   ps)
               (vl-println-main-fn x ps)))

Theorem: vl-println-main-fn-vl-printable-equiv-congruence-on-x

(defthm vl-println-main-fn-vl-printable-equiv-congruence-on-x
        (implies (vl-printable-equiv x x-equiv)
                 (equal (vl-println-main-fn x ps)
                        (vl-println-main-fn x-equiv ps)))
        :rule-classes :congruence)