(hex-chars-to-hex-pair-list chars) → hex-pair-list
Function:
(defun hex-chars-to-hex-pair-list (chars) (declare (xargs :guard (str::hex-digit-char-list*p chars))) (let ((__function__ 'hex-chars-to-hex-pair-list)) (declare (ignorable __function__)) (cond ((null chars) nil) ((not (and (str::hex-digit-char-list*p chars) (consp chars) (consp (cdr chars)) (str::hex-digit-char-p (first chars)) (str::hex-digit-char-p (second chars)))) (reserrf "hex-char-codes-to-hex-pair-list: chars should be a true list of hex digits")) (t (let* ((hex-digit1 (make-hex-digit :get (first chars))) (hex-digit2 (make-hex-digit :get (second chars))) (first-hex-pair (make-hex-pair :1st hex-digit1 :2nd hex-digit2))) (if (not (str::hex-digit-char-list*p (cddr chars))) (reserrf "problem in hex-char-codes-to-hex-pair-list") (let ((rest-hex-pairs (hex-chars-to-hex-pair-list (cddr chars)))) (if (not (hex-pair-listp rest-hex-pairs)) (reserrf "problem in hex-char-codes-to-hex-pair-list 2") (cons first-hex-pair rest-hex-pairs)))))))))
Theorem:
(defthm hex-pair-list-resultp-of-hex-chars-to-hex-pair-list (b* ((hex-pair-list (hex-chars-to-hex-pair-list chars))) (hex-pair-list-resultp hex-pair-list)) :rule-classes :rewrite)