		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-ext-declon-list

Print a list of zero or more external declarations.

Signature
(print-ext-declon-list extdecls pstate) → new-pstate
Arguments: extdecls — Guard (ext-declon-listp extdecls).; pstate — Guard (pristatep pstate).
Returns: new-pstate — Type (pristatep new-pstate).

We separate them with blank lines.

Definitions and Theorems

Function: print-ext-declon-list

(defun print-ext-declon-list (extdecls pstate)
 (declare (xargs :guard (and (ext-declon-listp extdecls)
                             (pristatep pstate))))
 (declare
  (xargs
   :guard
   (and (ext-declon-list-unambp extdecls)
        (ext-declon-list-aidentp extdecls (pristate->gcc pstate)))))
 (let ((__function__ 'print-ext-declon-list))
   (declare (ignorable __function__))
   (b* (((when (endp extdecls))
         (pristate-fix pstate))
        (pstate (print-ext-declon (car extdecls)
                                  pstate)))
     (print-ext-declon-list (cdr extdecls)
                            pstate))))

Theorem: pristatep-of-print-ext-declon-list

(defthm pristatep-of-print-ext-declon-list
  (b* ((new-pstate (print-ext-declon-list extdecls pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: pristate->gcc-of-print-ext-declon-list

(defthm pristate->gcc-of-print-ext-declon-list
  (b* ((?new-pstate (print-ext-declon-list extdecls pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: print-ext-declon-list-of-ext-declon-list-fix-extdecls

(defthm print-ext-declon-list-of-ext-declon-list-fix-extdecls
  (equal (print-ext-declon-list (ext-declon-list-fix extdecls)
                                pstate)
         (print-ext-declon-list extdecls pstate)))

Theorem: print-ext-declon-list-ext-declon-list-equiv-congruence-on-extdecls

(defthm
 print-ext-declon-list-ext-declon-list-equiv-congruence-on-extdecls
 (implies (ext-declon-list-equiv extdecls extdecls-equiv)
          (equal (print-ext-declon-list extdecls pstate)
                 (print-ext-declon-list extdecls-equiv pstate)))
 :rule-classes :congruence)

Theorem: print-ext-declon-list-of-pristate-fix-pstate

(defthm print-ext-declon-list-of-pristate-fix-pstate
  (equal (print-ext-declon-list extdecls (pristate-fix pstate))
         (print-ext-declon-list extdecls pstate)))

Theorem: print-ext-declon-list-pristate-equiv-congruence-on-pstate

(defthm print-ext-declon-list-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-ext-declon-list extdecls pstate)
                  (print-ext-declon-list extdecls pstate-equiv)))
  :rule-classes :congruence)