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