Pretty-print a list of hexadecimal digits and underscores.
(print-hexdig/uscore-list dus) → part
Function:
(defun print-hexdig/uscore-list (dus) (declare (xargs :guard (hexdig/uscore-listp dus))) (let ((__function__ 'print-hexdig/uscore-list)) (declare (ignorable __function__)) (cond ((endp dus) "") (t (msg "~@0~@1" (print-hexdig/uscore (car dus)) (print-hexdig/uscore-list (cdr dus)))))))
Theorem:
(defthm msgp-of-print-hexdig/uscore-list (b* ((part (print-hexdig/uscore-list dus))) (msgp part)) :rule-classes :rewrite)
Theorem:
(defthm print-hexdig/uscore-list-of-hexdig/uscore-list-fix-dus (equal (print-hexdig/uscore-list (hexdig/uscore-list-fix dus)) (print-hexdig/uscore-list dus)))
Theorem:
(defthm print-hexdig/uscore-list-hexdig/uscore-list-equiv-congruence-on-dus (implies (hexdig/uscore-list-equiv dus dus-equiv) (equal (print-hexdig/uscore-list dus) (print-hexdig/uscore-list dus-equiv))) :rule-classes :congruence)