• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
      • X86isa
      • Axe
      • Execloader
        • Elf-reader
        • Mach-o-reader
        • Merge-first-split-bytes
        • Split-bytes
        • Take-till-zero
        • Charlist->bytes
        • Merge-bytes
        • Bytes->charlist
          • String->bytes
          • Bytes->string
      • Math
      • Testing-utilities
    • Execloader

    Bytes->charlist

    Convert a list of bytes to a list of characters.

    Signature
    (bytes->charlist bytes) → lst
    Arguments
    bytes — Guard (byte-listp bytes).
    Returns
    lst — Type (character-listp lst), given (byte-listp bytes).

    Definitions and Theorems

    Function: bytes->charlist

    (defun bytes->charlist (bytes)
      (declare (xargs :guard (byte-listp bytes)))
      (let ((__function__ 'bytes->charlist))
        (declare (ignorable __function__))
        (if (endp bytes)
            nil
          (cons (code-char (car bytes))
                (bytes->charlist (cdr bytes))))))

    Theorem: character-listp-of-bytes->charlist

    (defthm character-listp-of-bytes->charlist
      (implies (byte-listp bytes)
               (b* ((lst (bytes->charlist bytes)))
                 (character-listp lst)))
      :rule-classes :rewrite)