		Search-engine friendly clone of the ACL2 documentation.

Hex-digit-char-listp

Recognize lists of hexadecimal digit characters.

Signature
(hex-digit-char-listp x) → std::bool

Unlike hex-digit-char-list*p, this requires true list (i.e. nil-terminated.

Since there are functions in std/strings that operate on hex-digit-char-list*p, we provide a bridge theorem between the two recognizers, which we can use to satisfy the guards of those functions.

Definitions and Theorems

Function: hex-digit-char-listp

(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)))
      (null x))))

Theorem: hex-digit-char-list*p-when-hex-digit-char-listp

(defthm hex-digit-char-list*p-when-hex-digit-char-listp
  (implies (hex-digit-char-listp x)
           (hex-digit-char-list*p x)))

Subtopics

Hex-digit-char-listp-basics: Basic theorems about hex-digit-char-listp, generated by std::deflist.
Hex-digit-char-listp-results: Theorems about results of std/strings functions that return lists of hexadecimal digit characters.