		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)