(cst2ast-hex-digit-char-list chars) → hex-digits
Function:
(defun cst2ast-hex-digit-char-list (chars) (declare (xargs :guard (str::hex-digit-char-list*p chars))) (let ((__function__ 'cst2ast-hex-digit-char-list)) (declare (ignorable __function__)) (cond ((not (and (str::hex-digit-char-list*p chars) (true-listp chars))) nil) ((endp chars) nil) (t (cons (make-hex-digit :get (car chars)) (cst2ast-hex-digit-char-list (cdr chars)))))))
Theorem:
(defthm hex-digit-listp-of-cst2ast-hex-digit-char-list (b* ((hex-digits (cst2ast-hex-digit-char-list chars))) (hex-digit-listp hex-digits)) :rule-classes :rewrite)