Recognize lists of octal digit characters.
(oct-digit-char-listp x) → std::bool
Unlike oct-digit-char-list*p,
this requires true list (i.e.
Since there are functions in std/strings that operate on oct-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 oct-digit-char-listp (x) (declare (xargs :guard t)) (let ((acl2::__function__ 'oct-digit-char-listp)) (declare (ignorable acl2::__function__)) (if (consp x) (and (oct-digit-char-p (car x)) (oct-digit-char-listp (cdr x))) (null x))))
Theorem:
(defthm oct-digit-char-list*p-when-oct-digit-char-listp (implies (oct-digit-char-listp x) (oct-digit-char-list*p x)))