		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)
                  ((atom x) (explode-atom x 10))
                  (t x))))
   (declare (type (integer 0 *) col))
   (if htmlp
    (b* ((tabsize (vl-ps->tabsize))
         ((mv & rchars)
          (if (stringp x)
              (vl-html-encode-string-aux x 0 (length x)
                                         col tabsize rchars)
            (vl-html-encode-chars-aux x col tabsize rchars))))
     (vl-ps-seq
          (vl-ps-update-rchars (revappend *vl-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)