		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-dexpo

Print a decimal exponent.

Signature
(print-dexpo expo pstate) → new-pstate
Arguments: expo — Guard (dexpop expo).; pstate — Guard (pristatep pstate).
Returns: new-pstate — Type (pristatep new-pstate).

We ensure that there is at least one digit.

Definitions and Theorems

Function: print-dexpo

(defun print-dexpo (expo pstate)
 (declare (xargs :guard (and (dexpop expo) (pristatep pstate))))
 (let ((__function__ 'print-dexpo))
  (declare (ignorable __function__))
  (b*
   (((dexpo expo) expo)
    (pstate (print-dexprefix expo.prefix pstate))
    (pstate (print-sign-option expo.sign? pstate))
    ((unless expo.digits)
     (raise
      "Misusage error: ~
                the decimal exponent has no digits.")
     pstate)
    (pstate (print-dec-digit-achars expo.digits pstate)))
   pstate)))

Theorem: pristatep-of-print-dexpo

(defthm pristatep-of-print-dexpo
  (b* ((new-pstate (print-dexpo expo pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: pristate->gcc-of-print-dexpo

(defthm pristate->gcc-of-print-dexpo
  (b* ((?new-pstate (print-dexpo expo pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: print-dexpo-of-dexpo-fix-expo

(defthm print-dexpo-of-dexpo-fix-expo
  (equal (print-dexpo (dexpo-fix expo) pstate)
         (print-dexpo expo pstate)))

Theorem: print-dexpo-dexpo-equiv-congruence-on-expo

(defthm print-dexpo-dexpo-equiv-congruence-on-expo
  (implies (dexpo-equiv expo expo-equiv)
           (equal (print-dexpo expo pstate)
                  (print-dexpo expo-equiv pstate)))
  :rule-classes :congruence)

Theorem: print-dexpo-of-pristate-fix-pstate

(defthm print-dexpo-of-pristate-fix-pstate
  (equal (print-dexpo expo (pristate-fix pstate))
         (print-dexpo expo pstate)))

Theorem: print-dexpo-pristate-equiv-congruence-on-pstate

(defthm print-dexpo-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-dexpo expo pstate)
                  (print-dexpo expo pstate-equiv)))
  :rule-classes :congruence)