		Search-engine friendly clone of the ACL2 documentation.

Basic-printing

Vl-println-markup

(vl-println-markup x &key (ps 'ps)) prints verbatim text with no encoding, then prints a newline.

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

This is identical to vl-print-markup except for the newline. Unlike vl-println, no <br/> tag is printed in HTML mode. The goal is only to provide a convenient way to insert line breaks in the middle of a lot of markup.

Definitions and Theorems

Function: vl-println-markup-fn

(defun
 vl-println-markup-fn (x ps)
 (declare (xargs :stobjs (ps)))
 (declare (xargs :guard (vl-printable-p x)))
 (let
  ((__function__ 'vl-println-markup))
  (declare (ignorable __function__))
  (let*
   ((rchars (vl-ps->rchars))
    (x (vl-printable-fix x)))
   (cond
    ((stringp x)
     (vl-ps-seq
          (vl-ps-update-rchars (cons #\Newline (cons x rchars)))
          (vl-ps-update-col 0)))
    ((and (atom x) x)
     (vl-ps-seq (vl-ps-update-rchars
                     (cons #\Newline
                           (revappend (explode-atom x 10) rchars)))
                (vl-ps-update-col 0)))
    (t
     (vl-ps-seq
         (vl-ps-update-rchars (cons #\Newline (revappend x rchars)))
         (vl-ps-update-col 0)))))))

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

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

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

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