		Search-engine friendly clone of the ACL2 documentation.

Execloader

String->bytes

Convert a string to a list of bytes.

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

Definitions and Theorems

Function: string->bytes

(defun string->bytes (str)
       (declare (xargs :guard (stringp str)))
       (let ((__function__ 'string->bytes))
            (declare (ignorable __function__))
            (charlist->bytes (coerce str 'list))))

Theorem: byte-listp-of-string->bytes

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