		Search-engine friendly clone of the ACL2 documentation.

Pretty-printing-implementation

Print-escaped-symbol

Signature
(print-escaped-symbol x config acc) → new-acc
Arguments: x — Guard (symbolp x).; config — Guard (printconfig-p config).
Returns: new-acc — Type (character-listp new-acc), given (character-listp acc).

Definitions and Theorems

Function: print-escaped-symbol$inline

(defun print-escaped-symbol$inline (x config acc)
 (declare (xargs :guard (and (symbolp x)
                             (printconfig-p config))))
 (let ((acl2::__function__ 'print-escaped-symbol))
  (declare (ignorable acl2::__function__))
  (b*
   ((name (symbol-name x))
    (lowercase-p (printconfig->print-lowercase config))
    (acc
      (b*
       (((when (keywordp x)) (cons #\: acc))
        ((when (in-home-package-p x config))
         acc)
        (pkg-name (symbol-package-name x))
        ((when (my-needs-slashes pkg-name config))
         (let* ((acc (cons #\| acc))
                (acc (print-escaped-str pkg-name #\| acc)))
           (list* #\: #\: #\| acc)))
        ((when lowercase-p)
         (let*
             ((acc (downcase-string-aux pkg-name 0 (length pkg-name)
                                        acc)))
           (list* #\: #\: acc))))
       (let* ((acc (revappend-chars pkg-name acc)))
         (list* #\: #\: acc))))
    ((when (my-needs-slashes name config))
     (let* ((acc (cons #\| acc))
            (acc (print-escaped-str name #\| acc)))
       (cons #\| acc)))
    ((when lowercase-p)
     (downcase-string-aux name 0 (length name)
                          acc)))
   (revappend-chars name acc))))

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

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