		Search-engine friendly clone of the ACL2 documentation.

Pretty-printing-implementation

Basic-print-rat

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

Signature
(basic-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: basic-print-rat

(defun basic-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__ 'basic-print-rat))
    (declare (ignorable acl2::__function__))
    (b* ((acc (basic-print-int (numerator x)
                               base acc))
         (acc (cons #\/ acc)))
      (basic-print-nat (denominator x)
                       base acc))))

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

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