		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-printer

Pprint-other

Print a character that does not fit any lexeme after preprocessing.

Signature
(pprint-other char bytes) → new-bytes
Arguments: char — Guard (natp char).; bytes — Guard (byte-listp bytes).
Returns: new-bytes — Type (byte-listp new-bytes).

This is for the :other case of plexeme.

Definitions and Theorems

Function: pprint-other

(defun pprint-other (char bytes)
  (declare (xargs :guard (and (natp char) (byte-listp bytes))))
  (let ((__function__ 'pprint-other))
    (declare (ignorable __function__))
    (b* (((unless (grammar-character-p char))
          (raise "Internal error: bad character code ~x0."
                 (nfix char))))
      (pprint-char char bytes))))

Theorem: byte-listp-of-pprint-other

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