		Search-engine friendly clone of the ACL2 documentation.

Execloader

Charlist->bytes

Convert a list of characters to a list of bytes.

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

Definitions and Theorems

Function: charlist->bytes

(defun charlist->bytes (charlist)
  (declare (xargs :guard (character-listp charlist)))
  (let ((__function__ 'charlist->bytes))
    (declare (ignorable __function__))
    (if (endp charlist)
        nil
      (cons (char-code (car charlist))
            (charlist->bytes (cdr charlist))))))

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

(defthm byte-listp-of-charlist->bytes
  (implies (and (character-listp charlist))
           (b* ((bl (charlist->bytes charlist)))
             (byte-listp bl)))
  :rule-classes :rewrite)

Theorem: same-length-of-byte-and-character-lists

(defthm same-length-of-byte-and-character-lists
  (b* ((?bl (charlist->bytes charlist)))
    (implies (character-listp charlist)
             (equal (len bl) (len charlist)))))