		Search-engine friendly clone of the ACL2 documentation.

Print-escaped-str

Print-escaped-str-aux

Signature
(print-escaped-str-aux x n xl slash-char acc) → *

Definitions and Theorems

Function: print-escaped-str-aux

(defun print-escaped-str-aux (x n xl slash-char acc)
 (declare (type string x)
          (type unsigned-byte n)
          (type unsigned-byte xl)
          (type character slash-char))
 (declare (xargs :guard (and (eql xl (length x)) (<= n xl))))
 (let ((acl2::__function__ 'print-escaped-str-aux))
  (declare (ignorable acl2::__function__))
  (b* (((when (mbe :logic (zp (- (length x) (nfix n)))
                   :exec (eql n xl)))
        acc)
       ((the character c1) (char x n))
       ((the unsigned-byte n)
        (+ 1
           (the unsigned-byte
                (mbe :logic (nfix n) :exec n)))))
    (print-escaped-str-aux x n xl slash-char
                           (if (or (eql c1 #\\) (eql c1 slash-char))
                               (list* c1 #\\ acc)
                             (cons c1 acc))))))

Theorem: print-escaped-str-aux-removal

(defthm print-escaped-str-aux-removal
  (implies (and (stringp x)
                (natp n)
                (equal xl (length x))
                (<= n xl))
           (equal (print-escaped-str-aux x n xl slash-char acc)
                  (print-escaped-charlist (nthcdr n (explode x))
                                          slash-char acc))))