(4vec-to-bitwise-chars upper lower width) → chars
Function:
(defun 4vec-to-bitwise-chars (upper lower width) (declare (xargs :guard (and (integerp upper) (integerp lower) (natp width)))) (let ((__function__ '4vec-to-bitwise-chars)) (declare (ignorable __function__)) (b* (((when (zp width)) nil) (width (1- width)) (up (logbitp width upper)) (low (logbitp width lower)) (char (if up (if low #\1 #\x) (if low #\z #\0)))) (cons char (4vec-to-bitwise-chars upper lower width)))))
Theorem:
(defthm character-listp-of-4vec-to-bitwise-chars (b* ((chars (4vec-to-bitwise-chars upper lower width))) (character-listp chars)) :rule-classes :rewrite)