		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-h-char-list

Print a list of zero or more characters usable in header names in angle brackets.

Signature
(print-h-char-list hchars pstate) → new-pstate
Arguments: hchars — Guard (h-char-listp hchars).; pstate — Guard (pristatep pstate).
Returns: new-pstate — Type (pristatep new-pstate).

Definitions and Theorems

Function: print-h-char-list

(defun print-h-char-list (hchars pstate)
  (declare (xargs :guard (and (h-char-listp hchars)
                              (pristatep pstate))))
  (let ((__function__ 'print-h-char-list))
    (declare (ignorable __function__))
    (b* (((when (endp hchars))
          (pristate-fix pstate))
         (pstate (print-h-char (car hchars) pstate)))
      (print-h-char-list (cdr hchars)
                         pstate))))

Theorem: pristatep-of-print-h-char-list

(defthm pristatep-of-print-h-char-list
  (b* ((new-pstate (print-h-char-list hchars pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: pristate->gcc-of-print-h-char-list

(defthm pristate->gcc-of-print-h-char-list
  (b* ((?new-pstate (print-h-char-list hchars pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: print-h-char-list-of-h-char-list-fix-hchars

(defthm print-h-char-list-of-h-char-list-fix-hchars
  (equal (print-h-char-list (h-char-list-fix hchars)
                            pstate)
         (print-h-char-list hchars pstate)))

Theorem: print-h-char-list-h-char-list-equiv-congruence-on-hchars

(defthm print-h-char-list-h-char-list-equiv-congruence-on-hchars
  (implies (h-char-list-equiv hchars hchars-equiv)
           (equal (print-h-char-list hchars pstate)
                  (print-h-char-list hchars-equiv pstate)))
  :rule-classes :congruence)

Theorem: print-h-char-list-of-pristate-fix-pstate

(defthm print-h-char-list-of-pristate-fix-pstate
  (equal (print-h-char-list hchars (pristate-fix pstate))
         (print-h-char-list hchars pstate)))

Theorem: print-h-char-list-pristate-equiv-congruence-on-pstate

(defthm print-h-char-list-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-h-char-list hchars pstate)
                  (print-h-char-list hchars pstate-equiv)))
  :rule-classes :congruence)