		Search-engine friendly clone of the ACL2 documentation.

Program-execution

Chars-to-c-str

Signature
(chars-to-c-str char-lst) → c-str
Arguments: char-lst — Guard (character-listp char-lst).
Returns: c-str — Type (byte-listp c-str).

Definitions and Theorems

Function: chars-to-c-str

(defun chars-to-c-str (char-lst)
  (declare (xargs :guard (character-listp char-lst)))
  (let ((__function__ 'chars-to-c-str))
    (declare (ignorable __function__))
    (if (mbt (character-listp char-lst))
        (if (not char-lst)
            '(0)
          (cons (char-code (car char-lst))
                (chars-to-c-str (cdr char-lst))))
      nil)))

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

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