(4vec-to-xml-chars x) → chars
Function:
(defun 4vec-to-xml-chars (x) (declare (xargs :guard (4vec-p x))) (let ((__function__ '4vec-to-xml-chars)) (declare (ignorable __function__)) (if (2vec-p x) (b* ((val (2vec->val x)) (val (loghead (integer-length val) val))) (if (< val 10) (str::nat-to-dec-chars val) (list* #\0 #\x (str::nat-to-hex-chars val)))) (b* (((4vec x) x) (len (max (integer-length x.upper) (integer-length x.lower))) ((when (and (<= len 6) (<= (integer-length x.lower) 6))) (list* #\0 #\b (4vec-to-bitwise-chars x.upper x.lower len)))) (list* #\0 #\x (4vec-to-hex-chars x.upper x.lower len))))))
Theorem:
(defthm character-listp-of-4vec-to-xml-chars (b* ((chars (4vec-to-xml-chars x))) (character-listp chars)) :rule-classes :rewrite)