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