Print a hexadecimal core floating constant.
(print-hex-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-hex-frac-const.
Function:
(defun print-hex-core-fconst (fconst pstate) (declare (xargs :guard (and (hex-core-fconstp fconst) (pristatep pstate)))) (let ((__function__ 'print-hex-core-fconst)) (declare (ignorable __function__)) (hex-core-fconst-case fconst :frac (b* ((pstate (print-hex-frac-const fconst.significand pstate)) (pstate (print-bin-expo fconst.expo pstate))) pstate) :int (b* (((unless fconst.significand) (raise "Misusage error: ~ the integer hexadecimal core floating constant ~ has no digits in the significand.") (pristate-fix pstate)) (pstate (print-hex-digit-achars fconst.significand pstate)) (pstate (print-bin-expo fconst.expo pstate))) pstate))))
Theorem:
(defthm pristatep-of-print-hex-core-fconst (b* ((new-pstate (print-hex-core-fconst fconst pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm print-hex-core-fconst-of-hex-core-fconst-fix-fconst (equal (print-hex-core-fconst (hex-core-fconst-fix fconst) pstate) (print-hex-core-fconst fconst pstate)))
Theorem:
(defthm print-hex-core-fconst-hex-core-fconst-equiv-congruence-on-fconst (implies (hex-core-fconst-equiv fconst fconst-equiv) (equal (print-hex-core-fconst fconst pstate) (print-hex-core-fconst fconst-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-hex-core-fconst-of-pristate-fix-pstate (equal (print-hex-core-fconst fconst (pristate-fix pstate)) (print-hex-core-fconst fconst pstate)))
Theorem:
(defthm print-hex-core-fconst-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-hex-core-fconst fconst pstate) (print-hex-core-fconst fconst pstate-equiv))) :rule-classes :congruence)