Evaluate a list of string elements to a list of bytes.
(eval-string-element-list elems) → bytes
We concatenate the lists of bytes for the elements.
Function:
(defun eval-string-element-list (elems) (declare (xargs :guard (string-element-listp elems))) (let ((__function__ 'eval-string-element-list)) (declare (ignorable __function__)) (cond ((endp elems) nil) (t (append (eval-string-element (car elems)) (eval-string-element-list (cdr elems)))))))
Theorem:
(defthm ubyte8-listp-of-eval-string-element-list (b* ((bytes (eval-string-element-list elems))) (acl2::ubyte8-listp bytes)) :rule-classes :rewrite)
Theorem:
(defthm eval-string-element-list-of-string-element-list-fix-elems (equal (eval-string-element-list (string-element-list-fix elems)) (eval-string-element-list elems)))
Theorem:
(defthm eval-string-element-list-string-element-list-equiv-congruence-on-elems (implies (string-element-list-equiv elems elems-equiv) (equal (eval-string-element-list elems) (eval-string-element-list elems-equiv))) :rule-classes :congruence)