• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • 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
      • Pad-trim
      • Coercion
        • Explode
        • Implode
        • Std/strings/make-character-list
        • Std/strings/coerce
      • Std/strings/digit-to-char
      • Substitution
      • Symbols
    • Std/io
    • Std/osets
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 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))))