		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)