Print a hexadecimal fractional constant.
(print-hex-frac-const hfconst pstate) → new-pstate
We ensure that there is at least one digit, before or after the fractional point.
Function:
(defun print-hex-frac-const (hfconst pstate) (declare (xargs :guard (and (hex-frac-constp hfconst) (pristatep pstate)))) (let ((__function__ 'print-hex-frac-const)) (declare (ignorable __function__)) (b* (((hex-frac-const hfconst) hfconst) ((unless (or hfconst.before hfconst.after)) (raise "Misusage error: ~ the hexadecimal fractional constant has no digits.") (pristate-fix pstate)) (pstate (print-hex-digit-achars hfconst.before pstate)) (pstate (print-astring "." pstate)) (pstate (print-hex-digit-achars hfconst.after pstate))) pstate)))
Theorem:
(defthm pristatep-of-print-hex-frac-const (b* ((new-pstate (print-hex-frac-const hfconst pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm print-hex-frac-const-of-hex-frac-const-fix-hfconst (equal (print-hex-frac-const (hex-frac-const-fix hfconst) pstate) (print-hex-frac-const hfconst pstate)))
Theorem:
(defthm print-hex-frac-const-hex-frac-const-equiv-congruence-on-hfconst (implies (hex-frac-const-equiv hfconst hfconst-equiv) (equal (print-hex-frac-const hfconst pstate) (print-hex-frac-const hfconst-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-hex-frac-const-of-pristate-fix-pstate (equal (print-hex-frac-const hfconst (pristate-fix pstate)) (print-hex-frac-const hfconst pstate)))
Theorem:
(defthm print-hex-frac-const-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-hex-frac-const hfconst pstate) (print-hex-frac-const hfconst pstate-equiv))) :rule-classes :congruence)