		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-printer

Plexemes-to-bytes

Turn a list of preprocessor lexemes into a list of bytes.

Signature
(plexemes-to-bytes lexemes) → bytes
Arguments: lexemes — Guard (plexeme-listp lexemes).
Returns: bytes — Type (byte-listp bytes).

This is the top-level function of our printer. The reversed list of bytes is initialized to empty, and we call the top-level printing function, reversing the final byte list.

Definitions and Theorems

Function: plexemes-to-bytes

(defun plexemes-to-bytes (lexemes)
  (declare (xargs :guard (plexeme-listp lexemes)))
  (rev (pprint-lexeme-list lexemes nil)))

Theorem: byte-listp-of-plexemes-to-bytes

(defthm byte-listp-of-plexemes-to-bytes
  (b* ((bytes (plexemes-to-bytes lexemes)))
    (byte-listp bytes))
  :rule-classes :rewrite)