		Search-engine friendly clone of the ACL2 documentation.

Literal-evaluation

Eval-hex-pair

Evaluate a pair of hex digits to a byte.

Signature
(eval-hex-pair hp) → val
Arguments: hp — Guard (hex-pairp hp).
Returns: val — Type (acl2::ubyte8p val).

The digits are interpreted in big endian form.

Definitions and Theorems

Function: eval-hex-pair

(defun eval-hex-pair (hp)
  (declare (xargs :guard (hex-pairp hp)))
  (let ((__function__ 'eval-hex-pair))
    (declare (ignorable __function__))
    (str::hex-digit-chars-value
         (list (hex-digit->get (hex-pair->1st hp))
               (hex-digit->get (hex-pair->2nd hp))))))

Theorem: ubyte8p-of-eval-hex-pair

(defthm ubyte8p-of-eval-hex-pair
  (b* ((val (eval-hex-pair hp)))
    (acl2::ubyte8p val))
  :rule-classes :rewrite)

Theorem: eval-hex-pair-of-hex-pair-fix-hp

(defthm eval-hex-pair-of-hex-pair-fix-hp
  (equal (eval-hex-pair (hex-pair-fix hp))
         (eval-hex-pair hp)))

Theorem: eval-hex-pair-hex-pair-equiv-congruence-on-hp

(defthm eval-hex-pair-hex-pair-equiv-congruence-on-hp
  (implies (hex-pair-equiv hp hp-equiv)
           (equal (eval-hex-pair hp)
                  (eval-hex-pair hp-equiv)))
  :rule-classes :congruence)