		Search-engine friendly clone of the ACL2 documentation.

Svtv-doc

4vec-to-hex-char

Signature
(4vec-to-hex-char upper lower) → hex-char
Arguments: upper — Guard (natp upper).; lower — Guard (natp lower).
Returns: hex-char — Type (characterp hex-char).

Definitions and Theorems

Function: 4vec-to-hex-char

(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: characterp-of-4vec-to-hex-char

(defthm characterp-of-4vec-to-hex-char
  (b* ((hex-char (4vec-to-hex-char upper lower)))
    (characterp hex-char))
  :rule-classes :rewrite)