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