Remove the underscores from a list of hexadecimal digits and underscores.
(hexdig/uscores-to-digits dus) → ds
Any underscores in a
Function:
(defun hexdig/uscores-to-digits (dus) (declare (xargs :guard (hexdig/uscore-listp dus))) (let ((__function__ 'hexdig/uscores-to-digits)) (declare (ignorable __function__)) (b* (((when (endp dus)) nil) (du (car dus))) (hexdig/uscore-case du :digit (cons du.get (hexdig/uscores-to-digits (cdr dus))) :underscore (hexdig/uscores-to-digits (cdr dus))))))
Theorem:
(defthm hex-digit-listp-of-hexdig/uscores-to-digits (b* ((ds (hexdig/uscores-to-digits dus))) (hex-digit-listp ds)) :rule-classes :rewrite)
Theorem:
(defthm hexdig/uscores-to-digits-of-hexdig/uscore-list-fix-dus (equal (hexdig/uscores-to-digits (hexdig/uscore-list-fix dus)) (hexdig/uscores-to-digits dus)))
Theorem:
(defthm hexdig/uscores-to-digits-hexdig/uscore-list-equiv-congruence-on-dus (implies (hexdig/uscore-list-equiv dus dus-equiv) (equal (hexdig/uscores-to-digits dus) (hexdig/uscores-to-digits dus-equiv))) :rule-classes :congruence)