		Search-engine friendly clone of the ACL2 documentation.

Preprocessor

Vl-ppst-pad

Prefix for lines produced by the preprocessor.

Signature
(vl-ppst-pad &key (ppst 'ppst)) → pad
Returns: pad — Type (stringp pad).

Definitions and Theorems

Function: vl-ppst-pad-fn

(defun vl-ppst-pad-fn (ppst)
  (declare (xargs :stobjs (ppst)))
  (declare (xargs :guard t))
  (let ((__function__ 'vl-ppst-pad))
    (declare (ignorable __function__))
    (cat "["
         (str::lpadstr (vl-nice-bytes (vl-ppst->bytes))
                       6)
         "] "
         (implode (make-list (len (vl-ppst->includes))
                             :initial-element #\Space)))))

Theorem: stringp-of-vl-ppst-pad

(defthm stringp-of-vl-ppst-pad
  (b* ((pad (vl-ppst-pad-fn ppst)))
    (stringp pad))
  :rule-classes :type-prescription)