		Search-engine friendly clone of the ACL2 documentation.

Pprint-form-feed

Print a form feed after preprocessing.

Function: pprint-form-feed

(defun pprint-form-feed (bytes)
  (declare (xargs :guard (byte-listp bytes)))
  (pprint-char 12 bytes))

Theorem: byte-listp-of-pprint-form-feed

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