		Search-engine friendly clone of the ACL2 documentation.

Pretty-printing-implementation

Print-escaped-str

Print a string, escaping backslashes and some other character.

Signature
(print-escaped-str x slash-char acc) → new-acc
Arguments: x — String or symbol name to be printed.
Guard (stringp x).; slash-char — Extra character to escape. When printing escaped strings this is typically the " character; for printing symbol names it would typically be the | character.
Guard (characterp slash-char).
Returns: new-acc — Type (character-listp new-acc), given (character-listp acc).

Definitions and Theorems

Function: print-escaped-str$inline

(defun print-escaped-str$inline (x slash-char acc)
  (declare (xargs :guard (and (stringp x)
                              (characterp slash-char))))
  (let ((acl2::__function__ 'print-escaped-str))
    (declare (ignorable acl2::__function__))
    (mbe :logic (print-escaped-charlist (explode x)
                                        slash-char acc)
         :exec (print-escaped-str-aux x 0 (length (the string x))
                                      slash-char acc))))

Theorem: character-listp-of-print-escaped-str

(defthm character-listp-of-print-escaped-str
  (implies
       (character-listp acc)
       (b* ((new-acc (print-escaped-str$inline x slash-char acc)))
         (character-listp new-acc)))
  :rule-classes :rewrite)

Subtopics

Print-escaped-str-aux: Implementation of print-escaped-str.