		Search-engine friendly clone of the ACL2 documentation.

Hex-digit

Hex-digitp

Recognizer for hex-digit.

Signature
(hex-digitp x) → yes/no
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: hex-digitp

(defun hex-digitp (x)
  (declare (xargs :guard t))
  (let ((__function__ 'hex-digitp))
    (declare (ignorable __function__))
    (and (integerp x)
         (or (and (<= (char-code #\0) x)
                  (<= x (char-code #\9)))
             (and (<= (char-code #\A) x)
                  (<= x (char-code #\F)))
             (and (<= (char-code #\a) x)
                  (<= x (char-code #\f)))))))

Theorem: booleanp-of-hex-digitp

(defthm booleanp-of-hex-digitp
  (b* ((yes/no (hex-digitp x)))
    (booleanp yes/no))
  :rule-classes :rewrite)