Recognizes lists of hex-digit-char-p characters.
(hex-digit-char-listp x) → std::bool
This is an ordinary std::deflist. It is
"loose" in that it does not care whether
Function:
(defun hex-digit-char-listp (x) (declare (xargs :guard t)) (let ((acl2::__function__ 'hex-digit-char-listp)) (declare (ignorable acl2::__function__)) (if (consp x) (and (hex-digit-char-p (car x)) (hex-digit-char-listp (cdr x))) t)))
Theorem:
(defthm icharlisteqv-implies-equal-hex-digit-char-listp-1 (implies (icharlisteqv x x-equiv) (equal (hex-digit-char-listp x) (hex-digit-char-listp x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm character-listp-when-hex-digit-char-listp (implies (hex-digit-char-listp x) (equal (character-listp x) (true-listp x))) :rule-classes ((:rewrite :backchain-limit-lst 1)))