		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-bexpo

Print a binary exponent.

Signature
(print-bexpo expo pstate) → new-pstate
Arguments: expo — Guard (bexpop 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-bexpo

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

Theorem: pristatep-of-print-bexpo

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

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

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

Theorem: print-bexpo-of-bexpo-fix-expo

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

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

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

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

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

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

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