		Search-engine friendly clone of the ACL2 documentation.

Pretty-printing-implementation

Radix-print-rat

Print a (non-integer) rational in a particular print base, with radix.

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

Definitions and Theorems

Function: radix-print-rat

(defun radix-print-rat (x base acc)
  (declare (type ratio x)
           (type (unsigned-byte 5) base))
  (declare (xargs :guard (and (rationalp x)
                              (print-base-p base))))
  (declare (xargs :split-types t
                  :guard (not (integerp x))))
  (let ((acl2::__function__ 'radix-print-rat))
    (declare (ignorable acl2::__function__))
    (case base
      (10 (basic-print-rat x base (list* #\r #\0 #\1 #\# acc)))
      (16 (basic-print-rat x base (list* #\x #\# acc)))
      (8 (basic-print-rat x base (list* #\o #\# acc)))
      (otherwise (basic-print-rat x base (list* #\b #\# acc))))))

Theorem: character-listp-of-radix-print-rat

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