		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-chars

Print zero or more characters.

Signature
(print-chars chars pstate) → new-pstate
Arguments: chars — Guard (nat-listp chars).; pstate — Guard (pristatep pstate).
Returns: new-pstate — Type (pristatep new-pstate).

The characters are supplied in a list (of their codes). They are printed from left to right.

Definitions and Theorems

Function: print-chars

(defun print-chars (chars pstate)
  (declare (xargs :guard (and (nat-listp chars)
                              (pristatep pstate))))
  (declare (xargs :guard (grammar-character-listp chars)))
  (let ((__function__ 'print-chars))
    (declare (ignorable __function__))
    (b* (((when (endp chars))
          (pristate-fix pstate))
         (pstate (print-char (car chars) pstate)))
      (print-chars (cdr chars) pstate))))

Theorem: pristatep-of-print-chars

(defthm pristatep-of-print-chars
  (b* ((new-pstate (print-chars chars pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: print-chars-of-pristate-fix-pstate

(defthm print-chars-of-pristate-fix-pstate
  (equal (print-chars chars (pristate-fix pstate))
         (print-chars chars pstate)))

Theorem: print-chars-pristate-equiv-congruence-on-pstate

(defthm print-chars-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-chars chars pstate)
                  (print-chars chars pstate-equiv)))
  :rule-classes :congruence)