Print a decimal core floating constant.
(print-dec-core-fconst fconst pstate) → new-pstate
For an integer one, we ensure that there is at least one digit. For a fractional one, the check is performed in print-dec-frac-const.
Function:
(defun print-dec-core-fconst (fconst pstate) (declare (xargs :guard (and (dec-core-fconstp fconst) (pristatep pstate)))) (let ((__function__ 'print-dec-core-fconst)) (declare (ignorable __function__)) (dec-core-fconst-case fconst :frac (b* ((pstate (print-dec-frac-const fconst.significand pstate)) (pstate (print-dec-expo-option fconst.expo? pstate))) pstate) :int (b* (((unless fconst.significand) (raise "Misusage error: ~ the integer decimal core floating constant ~ has no digits in the significand.") (pristate-fix pstate)) (pstate (print-dec-digit-achars fconst.significand pstate)) (pstate (print-dec-expo fconst.expo pstate))) pstate))))
Theorem:
(defthm pristatep-of-print-dec-core-fconst (b* ((new-pstate (print-dec-core-fconst fconst pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm print-dec-core-fconst-of-dec-core-fconst-fix-fconst (equal (print-dec-core-fconst (dec-core-fconst-fix fconst) pstate) (print-dec-core-fconst fconst pstate)))
Theorem:
(defthm print-dec-core-fconst-dec-core-fconst-equiv-congruence-on-fconst (implies (dec-core-fconst-equiv fconst fconst-equiv) (equal (print-dec-core-fconst fconst pstate) (print-dec-core-fconst fconst-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-dec-core-fconst-of-pristate-fix-pstate (equal (print-dec-core-fconst fconst (pristate-fix pstate)) (print-dec-core-fconst fconst pstate)))
Theorem:
(defthm print-dec-core-fconst-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-dec-core-fconst fconst pstate) (print-dec-core-fconst fconst pstate-equiv))) :rule-classes :congruence)