Pretty-print a hexadecimal digit or underscore.
(print-hexdig/uscore du) → part
Function:
(defun print-hexdig/uscore (du) (declare (xargs :guard (hexdig/uscore-p du))) (let ((__function__ 'print-hexdig/uscore)) (declare (ignorable __function__)) (hexdig/uscore-case du :digit (print-hex-digit du.get) :underscore "_")))
Theorem:
(defthm msgp-of-print-hexdig/uscore (b* ((part (print-hexdig/uscore du))) (msgp part)) :rule-classes :rewrite)
Theorem:
(defthm print-hexdig/uscore-of-hexdig/uscore-fix-du (equal (print-hexdig/uscore (hexdig/uscore-fix du)) (print-hexdig/uscore du)))
Theorem:
(defthm print-hexdig/uscore-hexdig/uscore-equiv-congruence-on-du (implies (hexdig/uscore-equiv du du-equiv) (equal (print-hexdig/uscore du) (print-hexdig/uscore du-equiv))) :rule-classes :congruence)