		Search-engine friendly clone of the ACL2 documentation.

Program-execution

String-to-c-str

Signature
(string-to-c-str str) → c-str
Arguments: str — Guard (stringp str).
Returns: c-str — Type (byte-listp c-str).

Definitions and Theorems

Function: string-to-c-str

(defun string-to-c-str (str)
  (declare (xargs :guard (stringp str)))
  (let ((__function__ 'string-to-c-str))
    (declare (ignorable __function__))
    (b* ((lst (coerce str 'list)))
      (chars-to-c-str lst))))

Theorem: byte-listp-of-string-to-c-str

(defthm byte-listp-of-string-to-c-str
  (b* ((c-str (string-to-c-str str)))
    (byte-listp c-str))
  :rule-classes :rewrite)