		Search-engine friendly clone of the ACL2 documentation.

Loader

Vl-loadstate-pad

Prefix for lines produced by the loader.

Signature
(vl-loadstate-pad st) → pad
Arguments: st — Guard (vl-loadstate-p st).
Returns: pad — Type (stringp pad).

See vl-ppst-pad, this is basically the same except that in the loader proper we know there are no open includes.

Definitions and Theorems

Function: vl-loadstate-pad

(defun
    vl-loadstate-pad (st)
    (declare (xargs :guard (vl-loadstate-p st)))
    (let ((__function__ 'vl-loadstate-pad))
         (declare (ignorable __function__))
         (cat "{"
              (str::lpadstr (vl-nice-bytes (vl-loadstate->bytes st))
                            6)
              "} ")))

Theorem: stringp-of-vl-loadstate-pad

(defthm stringp-of-vl-loadstate-pad
        (b* ((pad (vl-loadstate-pad st)))
            (stringp pad))
        :rule-classes :type-prescription)