Print a decimal exponent.
We ensure that there is at least one digit.
Function:
(defun print-dec-expo (expo pstate) (declare (xargs :guard (and (dec-expop expo) (pristatep pstate)))) (let ((__function__ 'print-dec-expo)) (declare (ignorable __function__)) (b* (((dec-expo expo) expo) (pstate (print-dec-expo-prefix 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:
(defthm pristatep-of-print-dec-expo (b* ((new-pstate (print-dec-expo expo pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm print-dec-expo-of-dec-expo-fix-expo (equal (print-dec-expo (dec-expo-fix expo) pstate) (print-dec-expo expo pstate)))
Theorem:
(defthm print-dec-expo-dec-expo-equiv-congruence-on-expo (implies (dec-expo-equiv expo expo-equiv) (equal (print-dec-expo expo pstate) (print-dec-expo expo-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-dec-expo-of-pristate-fix-pstate (equal (print-dec-expo expo (pristate-fix pstate)) (print-dec-expo expo pstate)))
Theorem:
(defthm print-dec-expo-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-dec-expo expo pstate) (print-dec-expo expo pstate-equiv))) :rule-classes :congruence)