		Search-engine friendly clone of the ACL2 documentation.

Literal-evaluation

Eval-hex-string-content

Evaluate the content of a hex string.

Signature
(eval-hex-string-content content) → bytes
Arguments: content — Guard (hex-string-contentp content).
Returns: bytes — Type (ubyte8-listp bytes).

We return a byte for the first element, followed by zero or more bytes for the remaining elements.

Definitions and Theorems

Function: eval-hex-string-content

(defun eval-hex-string-content (content)
  (declare (xargs :guard (hex-string-contentp content)))
  (let ((__function__ 'eval-hex-string-content))
    (declare (ignorable __function__))
    (b* (((hex-string-content content) content))
      (cons (eval-hex-pair content.first)
            (eval-hex-string-rest-element-list content.rest)))))

Theorem: ubyte8-listp-of-eval-hex-string-content

(defthm ubyte8-listp-of-eval-hex-string-content
  (b* ((bytes (eval-hex-string-content content)))
    (ubyte8-listp bytes))
  :rule-classes :rewrite)

Theorem: eval-hex-string-content-of-hex-string-content-fix-content

(defthm eval-hex-string-content-of-hex-string-content-fix-content
  (equal (eval-hex-string-content (hex-string-content-fix content))
         (eval-hex-string-content content)))

Theorem: eval-hex-string-content-hex-string-content-equiv-congruence-on-content

(defthm
 eval-hex-string-content-hex-string-content-equiv-congruence-on-content
 (implies (hex-string-content-equiv content content-equiv)
          (equal (eval-hex-string-content content)
                 (eval-hex-string-content content-equiv)))
 :rule-classes :congruence)