Pretty-print a hexadecimal integer literal.
(print-hex-integer-literal lit) → part
Function:
(defun print-hex-integer-literal (lit) (declare (xargs :guard (hex-integer-literalp lit))) (let ((__function__ 'print-hex-integer-literal)) (declare (ignorable __function__)) (b* (((hex-integer-literal lit) lit)) (msg "~@0~@1~@2" (if lit.prefix-upcase-p "0X" "0x") (print-hexdig/uscore-list lit.digits/uscores) (print-optional-integer-type-suffix lit.suffix?)))))
Theorem:
(defthm msgp-of-print-hex-integer-literal (b* ((part (print-hex-integer-literal lit))) (msgp part)) :rule-classes :rewrite)
Theorem:
(defthm print-hex-integer-literal-of-hex-integer-literal-fix-lit (equal (print-hex-integer-literal (hex-integer-literal-fix lit)) (print-hex-integer-literal lit)))
Theorem:
(defthm print-hex-integer-literal-hex-integer-literal-equiv-congruence-on-lit (implies (hex-integer-literal-equiv lit lit-equiv) (equal (print-hex-integer-literal lit) (print-hex-integer-literal lit-equiv))) :rule-classes :congruence)