• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
      • Std/lists
      • Std/alists
      • Obags
      • Std/util
      • Std/strings
        • Pretty-printing
        • Printtree
        • Base64
        • Charset-p
        • Strtok!
        • Cases
        • Concatenation
        • Html-encoding
        • Character-kinds
        • Substrings
        • Strtok
        • Equivalences
        • Url-encoding
        • Lines
        • Explode-implode-equalities
        • Ordering
        • Numbers
          • Decimal
          • Hex
            • Parse-hex-from-string
            • Hex-digit-char-p
            • Nat-to-hex-chars
            • Parse-hex-from-charlist
            • Hex-digit-chars-value
              • Hex-digit-chars-value1
              • Hex-digit-char-value
              • Take-leading-hex-digit-chars
              • Hexify
              • Hex-digit-char-listp
              • Hex-digit-char-list*p
              • Hex-digit-string-p
              • Strval16
              • Skip-leading-hex-digits
              • Nat-to-hex-string
              • Hexify-width
              • Nonzero-hex-digit-char-p
              • Nat-to-hex-string-list
              • Revappend-nat-to-hex-chars
              • Hex-digit-to-char
              • Nat-to-hex-string-size
            • Octal
            • Binary
          • Pad-trim
          • Coercion
          • Std/strings/digit-to-char
          • Substitution
          • Symbols
        • Std/osets
        • Std/io
        • Std/basic
        • Std/system
        • Std/typed-lists
        • Std/bitsets
        • Std/testing
        • Std/typed-alists
        • Std/stobjs
      • Community
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Hex-digit-chars-value

    Hex-digit-chars-value1

    Signature
    (hex-digit-chars-value1 x val) → *
    Arguments
    x — Guard (hex-digit-char-list*p x).

    Definitions and Theorems

    Function: hex-digit-chars-value1

    (defun hex-digit-chars-value1 (x val)
      (declare (type unsigned-byte val))
      (declare (xargs :guard (hex-digit-char-list*p x)))
      (let ((acl2::__function__ 'hex-digit-chars-value1))
        (declare (ignorable acl2::__function__))
        (if (consp x)
            (hex-digit-chars-value1
                 (cdr x)
                 (the unsigned-byte
                      (+ (the (unsigned-byte 4)
                              (hex-digit-char-value (car x)))
                         (the unsigned-byte
                              (ash (mbe :logic (lnfix val) :exec val)
                                   4)))))
          (lnfix val))))