		Search-engine friendly clone of the ACL2 documentation.

Execloader

Bytes->string

Convert a list of bytes to a string.

Signature
(bytes->string bytes) → str
Arguments: bytes — Guard (byte-listp bytes).
Returns: str — Type (stringp str), given the guard.

Definitions and Theorems

Function: bytes->string

(defun bytes->string (bytes)
       (declare (xargs :guard (byte-listp bytes)))
       (let ((__function__ 'bytes->string))
            (declare (ignorable __function__))
            (coerce (bytes->charlist bytes)
                    'string)))

Theorem: stringp-of-bytes->string

(defthm stringp-of-bytes->string
        (implies (and (byte-listp bytes))
                 (b* ((str (bytes->string bytes)))
                     (stringp str)))
        :rule-classes :rewrite)