• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
      • Lint
      • Mlib
      • Server
      • Kit
      • Printer
        • Ps
        • Basic-printing
        • Verilog-printing
        • Printing-locally
        • Formatted-printing
        • Accessing-printed-output
        • Vl-printedlist
          • Vl-printedlist-fix
          • Vl-printedlist-p
            • Vl-printedlist-p-basics
            • Vl-printedlist-peek
            • Vl-printedlist-length
          • Vl-printedlist-equiv
          • Vl-printedlist->string
          • Vl-printed-p
        • Json-printing
      • Esim-vl
      • Well-formedness
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• Vl-printedlist

Vl-printedlist-p

(vl-printedlist-p x) recognizes lists where every element satisfies vl-printed-p.

Signature

(vl-printedlist-p x) → *

This is an ordinary deflist. It is "loose" in that it does not care whether x is nil-terminated.

Theorem: vl-printedlist-p-of-repeated-revappend

(defthm vl-printedlist-p-of-repeated-revappend
        (implies (and (vl-printedlist-p x)
                      (force (vl-printedlist-p y)))
                 (vl-printedlist-p (repeated-revappend n x y))))

Theorem: vl-printedlist-p-of-vl-html-encode-push

(defthm
 vl-printedlist-p-of-vl-html-encode-push
 (implies
    (vl-printedlist-p acc)
    (vl-printedlist-p (vl-html-encode-push char1 col tabsize acc))))

Theorem: vl-printedlist-p-of-vl-html-encode-chars-aux

(defthm
  vl-printedlist-p-of-vl-html-encode-chars-aux
  (implies
       (vl-printedlist-p acc)
       (vl-printedlist-p
            (mv-nth 1
                    (vl-html-encode-chars-aux x col tabsize acc)))))

Theorem: vl-printedlist-p-of-vl-html-encode-string-aux

(defthm
 vl-printedlist-p-of-vl-html-encode-string-aux
 (implies
  (vl-printedlist-p acc)
  (vl-printedlist-p
      (mv-nth 1
              (vl-html-encode-string-aux x n xl col tabsize acc)))))

Theorem: vl-printedlist-p-of-vl-url-encode-chars-aux

(defthm
     vl-printedlist-p-of-vl-url-encode-chars-aux
     (implies (vl-printedlist-p acc)
              (vl-printedlist-p (vl-url-encode-chars-aux x acc))))

Theorem: vl-printedlist-p-of-vl-url-encode-string-aux

(defthm
 vl-printedlist-p-of-vl-url-encode-string-aux
 (implies (vl-printedlist-p acc)
          (vl-printedlist-p (vl-url-encode-string-aux x n xl acc))))

Subtopics

Vl-printedlist-p-basics

Basic theorems about vl-printedlist-p, generated by deflist.

Vl-printedlist-peek

Extract the last character that was printed.

Vl-printedlist-length

Compute the total length of the list, in characters.