		Search-engine friendly clone of the ACL2 documentation.

8bitbytes-hexchars-conversions

Hexchars=>ubyte8

Convert two hexadecimal digit characters to an unsigned 8-bit byte.

Signature
(hexchars=>ubyte8 hi-char lo-char) → byte
Arguments: hi-char — Guard (str::hex-digit-char-p hi-char).; lo-char — Guard (str::hex-digit-char-p lo-char).
Returns: byte — Type (unsigned-byte-p 8 byte).

The most significant digit comes first, followed by the least significant one.

Definitions and Theorems

Function: hexchars=>ubyte8

(defun hexchars=>ubyte8 (hi-char lo-char)
  (declare (xargs :guard (and (str::hex-digit-char-p hi-char)
                              (str::hex-digit-char-p lo-char))))
  (let ((__function__ 'hexchars=>ubyte8))
    (declare (ignorable __function__))
    (b* ((hi-digit (str::hex-digit-char-value hi-char))
         (lo-digit (str::hex-digit-char-value lo-char)))
      (+ (* 16 hi-digit) lo-digit))))

Theorem: return-type-of-hexchars=>ubyte8

(defthm return-type-of-hexchars=>ubyte8
  (b* ((byte (hexchars=>ubyte8 hi-char lo-char)))
    (unsigned-byte-p 8 byte))
  :rule-classes :rewrite)

Subtopics

Ubyte8<=>hexchars-inverses-theorems: ubyte8=>hexchars and hexchars=>ubyte8 are mutual inverses.