Recognize lists of decimal digit characters.
(dec-digit-char-listp x) → std::bool
Unlike dec-digit-char-list*p,
this requires true list (i.e.
Since there are functions in std/strings that operate on dec-digit-char-list*p, we provide a bridge theorem between the two recognizers, which we can use to satisfy the guards of those functions.
Function:
(defun dec-digit-char-listp (x) (declare (xargs :guard t)) (let ((acl2::__function__ 'dec-digit-char-listp)) (declare (ignorable acl2::__function__)) (if (consp x) (and (dec-digit-char-p (car x)) (dec-digit-char-listp (cdr x))) (null x))))
Theorem:
(defthm dec-digit-char-list*p-when-dec-digit-char-listp (implies (dec-digit-char-listp x) (dec-digit-char-list*p x)))