		Search-engine friendly clone of the ACL2 documentation.

Print-atom

Print-atom-aux

Goofy helper function to handle the number case.

Signature
(print-atom-aux x config acc) → new-acc
Arguments: x — This very weird guard is because we can't just assume it's an acl2-numberp due to bad atoms.
Guard (and (atom x) (not (symbolp x)) (not (stringp x)) (not (characterp x))) .; config — Guard (printconfig-p config).
Returns: new-acc — Type (character-listp new-acc), given (character-listp acc).

Definitions and Theorems

Function: print-atom-aux$inline

(defun print-atom-aux$inline (x config acc)
  (declare (xargs :guard (and (and (atom x)
                                   (not (symbolp x))
                                   (not (stringp x))
                                   (not (characterp x)))
                              (printconfig-p config))))
  (let ((acl2::__function__ 'print-atom-aux))
    (declare (ignorable acl2::__function__))
    (b* (((printconfig config) config)
         ((when (integerp x))
          (if config.print-radix
              (radix-print-int x config.print-base acc)
            (basic-print-int x config.print-base acc)))
         ((when (rationalp x))
          (if config.print-radix
              (radix-print-rat x config.print-base acc)
            (basic-print-rat x config.print-base acc)))
         ((when (complex-rationalp x))
          (if config.print-radix
              (radix-print-complex x config.print-base acc)
            (basic-print-complex x config.print-base acc))))
      (raise "Bad atom")
      acc)))

Theorem: character-listp-of-print-atom-aux

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