		Search-engine friendly clone of the ACL2 documentation.

Strval16

Interpret a string as a hexadecimal number.

Signature
(strval16 x) → value?
Arguments: x — Guard (stringp x).
Returns: value? — Type (or (natp value?) (not value?)).

For example, (strval16 "1F") is 31. If the string is empty or has any non hexadecimal digit characters (0-9, A-F, a-f), we return nil.

Definitions and Theorems

Function: strval16

(defun strval16 (x)
  (declare (xargs :guard (stringp x)))
  (declare (type string x))
  (declare (xargs :split-types t))
  (let ((acl2::__function__ 'strval16))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (let ((chars (explode x)))
           (and (consp chars)
                (hex-digit-char-list*p chars)
                (hex-digit-chars-value chars)))
         :exec
         (b* (((the unsigned-byte xl) (length x))
              ((mv (the unsigned-byte val)
                   (the unsigned-byte len))
               (parse-hex-from-string x 0 0 0 xl)))
           (and (not (eql 0 len))
                (eql len xl)
                val)))))

Theorem: return-type-of-strval16

(defthm return-type-of-strval16
  (b* ((value? (strval16 x)))
    (or (natp value?) (not value?)))
  :rule-classes :type-prescription)

Theorem: istreqv-implies-equal-strval16-1

(defthm istreqv-implies-equal-strval16-1
  (implies (istreqv x x-equiv)
           (equal (strval16 x) (strval16 x-equiv)))
  :rule-classes (:congruence))