• 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
        • Pad-trim
        • Coercion
          • Explode
          • Implode
          • Std/strings/make-character-list
            • Std/strings/coerce
          • 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
    • Coercion
    • Make-character-list

    Std/strings/make-character-list

    Lemmas about make-character-list in the std/strings library.

    This function is normally not anything you would ever want to use. It is notable mainly for the role it plays in the completion axiom for coerce.

    Definitions and Theorems

    Theorem: make-character-list-when-atom

    (defthm make-character-list-when-atom
            (implies (atom x)
                     (equal (make-character-list x) nil)))

    Theorem: make-character-list-of-cons

    (defthm make-character-list-of-cons
            (equal (make-character-list (cons a x))
                   (cons (char-fix a)
                         (make-character-list x))))

    Theorem: consp-of-make-character-list

    (defthm consp-of-make-character-list
            (equal (consp (make-character-list x))
                   (consp x)))

    Theorem: make-character-list-under-iff

    (defthm make-character-list-under-iff
            (iff (make-character-list x) (consp x)))

    Theorem: len-of-make-character-list

    (defthm len-of-make-character-list
            (equal (len (make-character-list x))
                   (len x)))

    Theorem: make-character-list-when-character-listp

    (defthm make-character-list-when-character-listp
            (implies (character-listp x)
                     (equal (make-character-list x) x)))

    Theorem: character-listp-of-make-character-list

    (defthm character-listp-of-make-character-list
            (character-listp (make-character-list x)))

    Theorem: make-character-list-of-append

    (defthm make-character-list-of-append
            (equal (make-character-list (append x y))
                   (append (make-character-list x)
                           (make-character-list y))))

    Theorem: make-character-list-of-revappend

    (defthm make-character-list-of-revappend
            (equal (make-character-list (revappend x y))
                   (revappend (make-character-list x)
                              (make-character-list y))))