Print an optional decimal exponent.
(print-dec-expo-option expo? pstate) → new-pstate
If there is no decimal exponent, we print nothing.
Function:
(defun print-dec-expo-option (expo? pstate) (declare (xargs :guard (and (dec-expo-optionp expo?) (pristatep pstate)))) (let ((__function__ 'print-dec-expo-option)) (declare (ignorable __function__)) (dec-expo-option-case expo? :some (print-dec-expo expo?.val pstate) :none (pristate-fix pstate))))
Theorem:
(defthm pristatep-of-print-dec-expo-option (b* ((new-pstate (print-dec-expo-option expo? pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm print-dec-expo-option-of-dec-expo-option-fix-expo? (equal (print-dec-expo-option (dec-expo-option-fix expo?) pstate) (print-dec-expo-option expo? pstate)))
Theorem:
(defthm print-dec-expo-option-dec-expo-option-equiv-congruence-on-expo? (implies (dec-expo-option-equiv expo? expo?-equiv) (equal (print-dec-expo-option expo? pstate) (print-dec-expo-option expo?-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-dec-expo-option-of-pristate-fix-pstate (equal (print-dec-expo-option expo? (pristate-fix pstate)) (print-dec-expo-option expo? pstate)))
Theorem:
(defthm print-dec-expo-option-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-dec-expo-option expo? pstate) (print-dec-expo-option expo? pstate-equiv))) :rule-classes :congruence)