• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
      • Syntax
      • Loader
      • Warnings
      • Getting-started
      • Utilities
      • Printer
        • Ps
        • Verilog-printing
        • Basic-printing
          • Vl-println?
          • Vl-print
          • Vl-printable-p
          • Vl-col-after-printing-string
          • Vl-col-after-printing-chars
          • Vl-print-strings-with-commas
          • Vl-string-needs-html-encoding-p
          • Vl-println-markup
          • Vl-print-strings-as-lines
          • Vl-print-url
          • Vl-print-nat
          • Vl-indent
          • Vl-println
          • Vl-print-markup
          • Vl-ps-seq
          • Vl-cw-ps-seq
          • Vl-when-html
          • Vl-ps-span
        • Printing-locally
        • Formatted-printing
        • Accessing-printed-output
        • Json-printing
        • Vl-printedlist
      • Kit
      • Mlib
      • Transforms
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Basic-printing

Vl-print-strings-as-lines

(vl-print-strings-as-lines x &key (ps 'ps)) prints the elements of x, a string list, on separate lines.

Signature

(vl-print-strings-as-lines x &key (ps 'ps)) → ps

Arguments

x — Guard (string-listp x).

The output is automatically encoded, and <br/> tags are added to separate the lines when we are in the HTML output mode. Each string is printed on its own line, with no indenting and no automatic word wrapping.

Definitions and Theorems

Function: vl-print-strings-as-lines-fn

(defun vl-print-strings-as-lines-fn (x ps)
  (declare (xargs :stobjs (ps)))
  (declare (xargs :guard (string-listp x)))
  (let ((__function__ 'vl-print-strings-as-lines))
    (declare (ignorable __function__))
    (if (atom x)
        ps
      (vl-ps-seq (vl-println (string-fix (car x)))
                 (vl-print-strings-as-lines (cdr x))))))

Theorem: vl-print-strings-as-lines-fn-of-string-list-fix-x

(defthm vl-print-strings-as-lines-fn-of-string-list-fix-x
  (equal (vl-print-strings-as-lines-fn (string-list-fix x)
                                       ps)
         (vl-print-strings-as-lines-fn x ps)))

Theorem: vl-print-strings-as-lines-fn-string-list-equiv-congruence-on-x

(defthm
     vl-print-strings-as-lines-fn-string-list-equiv-congruence-on-x
  (implies (str::string-list-equiv x x-equiv)
           (equal (vl-print-strings-as-lines-fn x ps)
                  (vl-print-strings-as-lines-fn x-equiv ps)))
  :rule-classes :congruence)