• 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
          • Octal
            • Parse-octal-from-string
            • Parse-octal-from-charlist
            • Nat-to-oct-chars
            • Oct-digit-chars-value
            • Oct-digit-char-p
            • Take-leading-oct-digit-chars
            • Oct-digit-char-value
            • Oct-digit-char-list*p
            • Oct-digit-char-listp
            • Skip-leading-octal-digits
            • Oct-digit-string-p
            • Nat-to-oct-string
              • Strval8
              • Nat-to-oct-string-list
              • Revappend-nat-to-oct-chars
              • Nonzero-oct-digit-char-p
              • Nat-to-oct-string-size
              • Octal-digit-to-char
            • 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
    • Octal

    Nat-to-oct-string

    Convert a natural number into a string with its octal digits.

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

    For instance, (nat-to-oct-string 15) is "17".

    Definitions and Theorems

    Function: nat-to-oct-string$inline

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

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

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

    Theorem: oct-digit-char-list*p-of-nat-to-dec-string

    (defthm oct-digit-char-list*p-of-nat-to-dec-string
      (oct-digit-char-list*p (explode (nat-to-oct-string n))))

    Theorem: nat-to-oct-string-one-to-one

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

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

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

    Theorem: nat-to-oct-string-nonempty

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