		Search-engine friendly clone of the ACL2 documentation.

Svtv-doc

4vec-to-xml-chars

Signature
(4vec-to-xml-chars x) → chars
Arguments: x — Guard (4vec-p x).
Returns: chars — Type (character-listp chars).

Definitions and Theorems

Function: 4vec-to-xml-chars

(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: character-listp-of-4vec-to-xml-chars

(defthm character-listp-of-4vec-to-xml-chars
  (b* ((chars (4vec-to-xml-chars x)))
    (character-listp chars))
  :rule-classes :rewrite)