		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-printer

Pprint-block-comment

Print a block comment after preprocessing.

Signature
(pprint-block-comment content bytes) → new-bytes
Arguments: content — Guard (nat-listp content).; bytes — Guard (byte-listp bytes).
Returns: new-bytes — Type (byte-listp new-bytes).

Definitions and Theorems

Function: pprint-block-comment

(defun pprint-block-comment (content bytes)
  (declare (xargs :guard (and (nat-listp content)
                              (byte-listp bytes))))
  (let ((__function__ 'pprint-block-comment))
    (declare (ignorable __function__))
    (b* ((bytes (pprint-astring "/*" bytes))
         ((unless (grammar-character-listp content))
          (raise "Internal error: bad block comment content ~x0."
                 (nat-list-fix content)))
         (bytes (pprint-chars content bytes))
         (bytes (pprint-astring "*/" bytes)))
      bytes)))

Theorem: byte-listp-of-pprint-block-comment

(defthm byte-listp-of-pprint-block-comment
  (b* ((new-bytes (pprint-block-comment content bytes)))
    (byte-listp new-bytes))
  :rule-classes :rewrite)