• 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
            • Parse-nat-from-string
            • Parse-nat-from-charlist
            • Nat-to-dec-chars
            • Dec-digit-chars-value
            • Dec-digit-char-p
            • Dec-digit-char-listp
            • Take-leading-dec-digit-chars
            • Dec-digit-char-value
              • Dec-digit-char-list*p
              • Nat-to-dec-string-width
              • Nat-to-dec-string
              • Dec-digit-string-p
              • Strval
              • Skip-leading-digits
              • Nat-to-dec-string-size
              • Int-to-dec-string-width
              • Int-to-dec-string
              • Nonzero-dec-digit-char-p
              • Nat-to-dec-string-list
              • Int-to-dec-string-list
              • Revappend-nat-to-dec-chars
            • Hex
            • 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
    • Decimal

    Dec-digit-char-value

    Coerces a dec-digit-char-p character into a number.

    Signature
    (dec-digit-char-value x) → val
    Arguments
    x — Guard (dec-digit-char-p x).
    Returns
    val — Type (natp val).

    For instance, (dec-digit-char-value #\3) is 3. For any non-dec-digit-char-p, 0 is returned.

    Definitions and Theorems

    Function: dec-digit-char-value$inline

    (defun dec-digit-char-value$inline (x)
      (declare (type character x))
      (declare (xargs :guard (dec-digit-char-p x)))
      (declare (xargs :split-types t))
      (let ((acl2::__function__ 'dec-digit-char-value))
        (declare (ignorable acl2::__function__))
        (mbe :logic
             (if (dec-digit-char-p x)
                 (- (char-code (char-fix x))
                    (char-code #\0))
               0)
             :exec (the (unsigned-byte 8)
                        (- (the (unsigned-byte 8)
                                (char-code (the character x)))
                           (the (unsigned-byte 8) 48))))))

    Theorem: natp-of-dec-digit-char-value

    (defthm natp-of-dec-digit-char-value
      (b* ((val (dec-digit-char-value$inline x)))
        (natp val))
      :rule-classes :type-prescription)

    Theorem: ichareqv-implies-equal-dec-digit-char-value-1

    (defthm ichareqv-implies-equal-dec-digit-char-value-1
      (implies (ichareqv x x-equiv)
               (equal (dec-digit-char-value x)
                      (dec-digit-char-value x-equiv)))
      :rule-classes (:congruence))

    Theorem: dec-digit-char-value-upper-bound

    (defthm dec-digit-char-value-upper-bound
      (< (dec-digit-char-value x) 10)
      :rule-classes ((:rewrite) (:linear)))

    Theorem: equal-of-dec-digit-char-value-and-dec-digit-char-value

    (defthm equal-of-dec-digit-char-value-and-dec-digit-char-value
      (implies (and (dec-digit-char-p x)
                    (dec-digit-char-p y))
               (equal (equal (dec-digit-char-value x)
                             (dec-digit-char-value y))
                      (equal x y))))

    Theorem: dec-digit-char-value-of-digit-to-char

    (defthm dec-digit-char-value-of-digit-to-char
      (implies (and (natp n) (< n 10))
               (equal (dec-digit-char-value (digit-to-char n))
                      n)))