		Search-engine friendly clone of the ACL2 documentation.

Pretty-printing-implementation

Basic-print-complex

Print a complex rational in a particular print base, no radix.

Signature
(basic-print-complex x base acc) → new-acc
Arguments: x — Guard (complex-rationalp x).; base — Guard (print-base-p base).
Returns: new-acc — Type (character-listp new-acc), given (character-listp acc).

Definitions and Theorems

Function: basic-print-complex

(defun basic-print-complex (x base acc)
  (declare (type complex x)
           (type (unsigned-byte 5) base))
  (declare (xargs :guard (and (complex-rationalp x)
                              (print-base-p base))))
  (declare (xargs :split-types t))
  (let ((acl2::__function__ 'basic-print-complex))
    (declare (ignorable acl2::__function__))
    (b* ((acc (list* #\( #\C #\# acc))
         (real (realpart x))
         (acc (if (integerp real)
                  (basic-print-int real base acc)
                (basic-print-rat real base acc)))
         (acc (cons #\Space acc))
         (imag (imagpart x))
         (acc (if (integerp imag)
                  (basic-print-int imag base acc)
                (basic-print-rat imag base acc))))
      (cons #\) acc))))

Theorem: character-listp-of-basic-print-complex

(defthm character-listp-of-basic-print-complex
  (implies (character-listp acc)
           (b* ((new-acc (basic-print-complex x base acc)))
             (character-listp new-acc)))
  :rule-classes :rewrite)