		Search-engine friendly clone of the ACL2 documentation.

Literal-evaluation

Eval-hex-string-rest-element-list

Evaluate a list of element of hex strings after the first one.

Signature
(eval-hex-string-rest-element-list elems) → bytes
Arguments: elems — Guard (hex-string-rest-element-listp elems).
Returns: bytes — Type (ubyte8-listp bytes).

This is done element-wise: each element is turned into a byte, and the order is preserved.

Definitions and Theorems

Function: eval-hex-string-rest-element-list

(defun eval-hex-string-rest-element-list (elems)
 (declare (xargs :guard (hex-string-rest-element-listp elems)))
 (let ((__function__ 'eval-hex-string-rest-element-list))
  (declare (ignorable __function__))
  (cond
       ((endp elems) nil)
       (t (cons (eval-hex-string-rest-element (car elems))
                (eval-hex-string-rest-element-list (cdr elems)))))))

Theorem: ubyte8-listp-of-eval-hex-string-rest-element-list

(defthm ubyte8-listp-of-eval-hex-string-rest-element-list
  (b* ((bytes (eval-hex-string-rest-element-list elems)))
    (ubyte8-listp bytes))
  :rule-classes :rewrite)

Theorem: eval-hex-string-rest-element-list-of-hex-string-rest-element-list-fix-elems

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

Theorem: eval-hex-string-rest-element-list-hex-string-rest-element-list-equiv-congruence-on-elems

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