		Search-engine friendly clone of the ACL2 documentation.

Literal-evaluation

Eval-hex-string-rest-element

Evaluate an element of hex strings after the first one.

Signature
(eval-hex-string-rest-element elem) → val
Arguments: elem — Guard (hex-string-rest-elementp elem).
Returns: val — Type (ubyte8p val).

This reduces to the evaluation of the pair of hex digits. The optional underscore is merely concrete syntactic information, retained in the abstract syntax but semantically irrelevant.

Definitions and Theorems

Function: eval-hex-string-rest-element

(defun eval-hex-string-rest-element (elem)
  (declare (xargs :guard (hex-string-rest-elementp elem)))
  (let ((__function__ 'eval-hex-string-rest-element))
    (declare (ignorable __function__))
    (eval-hex-pair (hex-string-rest-element->pair elem))))

Theorem: ubyte8p-of-eval-hex-string-rest-element

(defthm ubyte8p-of-eval-hex-string-rest-element
  (b* ((val (eval-hex-string-rest-element elem)))
    (ubyte8p val))
  :rule-classes :rewrite)

Theorem: eval-hex-string-rest-element-of-hex-string-rest-element-fix-elem

(defthm
   eval-hex-string-rest-element-of-hex-string-rest-element-fix-elem
 (equal
   (eval-hex-string-rest-element (hex-string-rest-element-fix elem))
   (eval-hex-string-rest-element elem)))

Theorem: eval-hex-string-rest-element-hex-string-rest-element-equiv-congruence-on-elem

(defthm
 eval-hex-string-rest-element-hex-string-rest-element-equiv-congruence-on-elem
 (implies (hex-string-rest-element-equiv elem elem-equiv)
          (equal (eval-hex-string-rest-element elem)
                 (eval-hex-string-rest-element elem-equiv)))
 :rule-classes :congruence)