		Search-engine friendly clone of the ACL2 documentation.

Pretty-printing-implementation

Print-atom

Print any arbitrary atom with no escaping, but obeying print-base, print-radix, and (for symbols) print-lowercase.

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

Definitions and Theorems

Function: print-atom

(defun print-atom (x config acc)
 (declare (xargs :guard (and (atom x) (printconfig-p config))))
 (let ((acl2::__function__ 'print-atom))
  (declare (ignorable acl2::__function__))
  (b* (((when (symbolp x))
        (let ((name (symbol-name x)))
          (if (printconfig->print-lowercase config)
              (downcase-string-aux name 0 (length (the string name))
                                   acc)
            (revappend-chars name acc))))
       ((when (characterp x)) (cons x acc))
       ((when (stringp x))
        (revappend-chars x acc)))
    (print-atom-aux x config acc))))

Theorem: character-listp-of-print-atom

(defthm character-listp-of-print-atom
  (implies (character-listp acc)
           (b* ((new-acc (print-atom x config acc)))
             (character-listp new-acc)))
  :rule-classes :rewrite)

Subtopics

Print-atom-aux: Goofy helper function to handle the number case.