		Search-engine friendly clone of the ACL2 documentation.

Pprint-spaces

Print one or more spaces after preprocessing.

Signature
(pprint-spaces count bytes) → new-bytes
Arguments: count — Guard (posp count).; bytes — Guard (byte-listp bytes).
Returns: new-bytes — Type (byte-listp new-bytes).

Function: pprint-spaces

(defun pprint-spaces (count bytes)
  (declare (xargs :guard (and (posp count) (byte-listp bytes))))
  (pprint-chars (repeat count 32) bytes))

Theorem: byte-listp-of-pprint-spaces

(defthm byte-listp-of-pprint-spaces
  (b* ((new-bytes (pprint-spaces count bytes)))
    (byte-listp new-bytes))
  :rule-classes :rewrite)