Evaluate a list of hex pairs to a list of bytes.
(eval-hex-pair-list hps) → bytes
This is done element-wise: each pair is turned into a byte, and the order is preserved.
Function:
(defun eval-hex-pair-list (hps) (declare (xargs :guard (hex-pair-listp hps))) (let ((__function__ 'eval-hex-pair-list)) (declare (ignorable __function__)) (cond ((endp hps) nil) (t (cons (eval-hex-pair (car hps)) (eval-hex-pair-list (cdr hps)))))))
Theorem:
(defthm ubyte8-listp-of-eval-hex-pair-list (b* ((bytes (eval-hex-pair-list hps))) (acl2::ubyte8-listp bytes)) :rule-classes :rewrite)
Theorem:
(defthm eval-hex-pair-list-of-hex-pair-list-fix-hps (equal (eval-hex-pair-list (hex-pair-list-fix hps)) (eval-hex-pair-list hps)))
Theorem:
(defthm eval-hex-pair-list-hex-pair-list-equiv-congruence-on-hps (implies (hex-pair-list-equiv hps hps-equiv) (equal (eval-hex-pair-list hps) (eval-hex-pair-list hps-equiv))) :rule-classes :congruence)