• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Debugging
    • Projects
    • Std
      • Std/lists
      • Std/alists
      • Obags
      • Std/util
      • Std/strings
        • Pretty-printing
        • Printtree
        • Base64
        • Strtok!
        • Charset-p
        • Cases
        • Concatenation
        • Html-encoding
        • Character-kinds
        • Substrings
        • Strtok
        • Equivalences
        • Url-encoding
        • Lines
        • Ordering
        • Numbers
          • Decimal
            • Parse-nat-from-string
            • Parse-nat-from-charlist
            • Nat-to-dec-chars
            • Dec-digit-chars-value
            • Dec-digit-char-p
            • Take-leading-dec-digit-chars
            • Dec-digit-char-value
            • Dec-digit-char-listp
            • 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
              • Nat-to-dec-string-list
              • Int-to-dec-string-list
              • Nonzero-dec-digit-char-p
              • Revappend-nat-to-dec-chars
            • Hex
            • Octal
            • Binary
          • Pad-trim
          • Coercion
          • Std/strings-extensions
          • Std/strings/digit-to-char
          • Substitution
          • Symbols
        • Std/io
        • Std/osets
        • Std/system
        • Std/basic
        • Std/typed-lists
        • Std/bitsets
        • Std/testing
        • Std/typed-alists
        • Std/stobjs
        • Std-extensions
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Decimal

    Nat-to-dec-string

    Convert a natural number into a string with its digits.

    Signature
    (nat-to-dec-string n) → str
    Arguments
    n — Guard (natp n).
    Returns
    str — Type (stringp str).

    For instance, (nat-to-dec-string 123) is "123".

    Definitions and Theorems

    Function: nat-to-dec-string$inline

    (defun nat-to-dec-string$inline (n)
           (declare (xargs :guard (natp n)))
           (let ((acl2::__function__ 'nat-to-dec-string))
                (declare (ignorable acl2::__function__))
                (implode (nat-to-dec-chars n))))

    Theorem: stringp-of-nat-to-dec-string

    (defthm stringp-of-nat-to-dec-string
            (b* ((str (nat-to-dec-string$inline n)))
                (stringp str))
            :rule-classes :type-prescription)

    Theorem: dec-digit-char-listp-of-nat-to-dec-string

    (defthm dec-digit-char-listp-of-nat-to-dec-string
            (dec-digit-char-listp (explode (nat-to-dec-string n))))

    Theorem: nat-to-dec-string-one-to-one

    (defthm nat-to-dec-string-one-to-one
            (equal (equal (nat-to-dec-string n)
                          (nat-to-dec-string m))
                   (equal (nfix n) (nfix m))))

    Theorem: dec-digit-chars-value-of-nat-to-dec-string

    (defthm
         dec-digit-chars-value-of-nat-to-dec-string
         (equal (dec-digit-chars-value (explode (nat-to-dec-string n)))
                (nfix n)))

    Theorem: nat-to-dec-string-nonempty

    (defthm nat-to-dec-string-nonempty
            (not (equal (nat-to-dec-string n) "")))