		Search-engine friendly clone of the ACL2 documentation.

Literal-evaluation

Eval-hex-quad

Evaluate a quadruple of hex digits to a 16-bit unsigned integer.

Signature
(eval-hex-quad hq) → val
Arguments: hq — Guard (hex-quadp hq).
Returns: val — Type (ubyte16p val).

The digits are interpreted in big endian form.

Definitions and Theorems

Function: eval-hex-quad

(defun eval-hex-quad (hq)
  (declare (xargs :guard (hex-quadp hq)))
  (let ((__function__ 'eval-hex-quad))
    (declare (ignorable __function__))
    (str::hex-digit-chars-value
         (list (hex-digit->get (hex-quad->1st hq))
               (hex-digit->get (hex-quad->2nd hq))
               (hex-digit->get (hex-quad->3rd hq))
               (hex-digit->get (hex-quad->4th hq))))))

Theorem: ubyte16p-of-eval-hex-quad

(defthm ubyte16p-of-eval-hex-quad
  (b* ((val (eval-hex-quad hq)))
    (ubyte16p val))
  :rule-classes :rewrite)

Theorem: eval-hex-quad-of-hex-quad-fix-hq

(defthm eval-hex-quad-of-hex-quad-fix-hq
  (equal (eval-hex-quad (hex-quad-fix hq))
         (eval-hex-quad hq)))

Theorem: eval-hex-quad-hex-quad-equiv-congruence-on-hq

(defthm eval-hex-quad-hex-quad-equiv-congruence-on-hq
  (implies (hex-quad-equiv hq hq-equiv)
           (equal (eval-hex-quad hq)
                  (eval-hex-quad hq-equiv)))
  :rule-classes :congruence)