		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-printer

Pprint-s-char

Print a character or escape sequence usable in string literals, after preprocessing.

Signature
(pprint-s-char schar bytes) → new-bytes
Arguments: schar — Guard (s-char-p schar).; bytes — Guard (byte-listp bytes).
Returns: new-bytes — Type (byte-listp new-bytes).

Definitions and Theorems

Function: pprint-s-char

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

Theorem: byte-listp-of-pprint-s-char

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