Print a decimal exponent prefix.
(print-dec-expo-prefix prefix pstate) → new-pstate
Function:
(defun print-dec-expo-prefix (prefix pstate) (declare (xargs :guard (and (dec-expo-prefixp prefix) (pristatep pstate)))) (let ((__function__ 'print-dec-expo-prefix)) (declare (ignorable __function__)) (dec-expo-prefix-case prefix :locase-e (print-astring "e" pstate) :upcase-e (print-astring "E" pstate))))
Theorem:
(defthm pristatep-of-print-dec-expo-prefix (b* ((new-pstate (print-dec-expo-prefix prefix pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm print-dec-expo-prefix-of-dec-expo-prefix-fix-prefix (equal (print-dec-expo-prefix (dec-expo-prefix-fix prefix) pstate) (print-dec-expo-prefix prefix pstate)))
Theorem:
(defthm print-dec-expo-prefix-dec-expo-prefix-equiv-congruence-on-prefix (implies (dec-expo-prefix-equiv prefix prefix-equiv) (equal (print-dec-expo-prefix prefix pstate) (print-dec-expo-prefix prefix-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-dec-expo-prefix-of-pristate-fix-pstate (equal (print-dec-expo-prefix prefix (pristate-fix pstate)) (print-dec-expo-prefix prefix pstate)))
Theorem:
(defthm print-dec-expo-prefix-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-dec-expo-prefix prefix pstate) (print-dec-expo-prefix prefix pstate-equiv))) :rule-classes :congruence)