(4vec-to-hex-char upper lower) → hex-char
Function:
(defun 4vec-to-hex-char (upper lower) (declare (xargs :guard (and (natp upper) (natp lower)))) (declare (xargs :guard (and (< upper 16) (< lower 16)))) (let ((__function__ '4vec-to-hex-char)) (declare (ignorable __function__)) (b* ((upper (lnfix upper)) (lower (lnfix lower))) (cond ((eql upper lower) (if (< upper 10) (code-char (+ (char-code #\0) upper)) (code-char (+ (char-code #\A) (- upper 10))))) ((and (eql upper 15) (eql lower 0)) #\X) ((and (eql upper 0) (eql lower 15)) #\Z) ((eql 0 (logand upper (lognot lower))) #\z) (t #\x)))))
Theorem:
(defthm characterp-of-4vec-to-hex-char (b* ((hex-char (4vec-to-hex-char upper lower))) (characterp hex-char)) :rule-classes :rewrite)