(4vec-to-hex-chars upper lower width) → chars
Function:
(defun 4vec-to-hex-chars (upper lower width) (declare (xargs :guard (and (integerp upper) (integerp lower) (natp width)))) (let ((__function__ '4vec-to-hex-chars)) (declare (ignorable __function__)) (b* (((when (zp width)) nil) (offset (logand (1- width) -4)) (nbits (- width offset)) (up (loghead nbits (logtail offset upper))) (low (loghead nbits (logtail offset lower)))) (cons (4vec-to-hex-char up low) (4vec-to-hex-chars upper lower offset)))))
Theorem:
(defthm character-listp-of-4vec-to-hex-chars (b* ((chars (4vec-to-hex-chars upper lower width))) (character-listp chars)) :rule-classes :rewrite)