		Search-engine friendly clone of the ACL2 documentation.

Pprint-vertical-tab

Print a vertical tab after preprocessing.

Function: pprint-vertical-tab

(defun pprint-vertical-tab (bytes)
  (declare (xargs :guard (byte-listp bytes)))
  (pprint-char 11 bytes))

Theorem: byte-listp-of-pprint-vertical-tab

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