		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-label-declaration-list

Print zero or more label declarations.

Signature
(print-label-declaration-list labelss pstate) → new-pstate
Arguments: labelss — Guard (ident-list-listp labelss).; pstate — Guard (pristatep pstate).
Returns: new-pstate — Type (pristatep new-pstate).

Definitions and Theorems

Function: print-label-declaration-list

(defun print-label-declaration-list (labelss pstate)
 (declare (xargs :guard (and (ident-list-listp labelss)
                             (pristatep pstate))))
 (declare
  (xargs
   :guard (ident-list-list-aidentp labelss (pristate->gcc pstate))))
 (let ((__function__ 'print-label-declaration-list))
  (declare (ignorable __function__))
  (b*
   (((when (endp labelss))
     (pristate-fix pstate))
    (labels (car labelss))
    ((unless (consp labels))
     (raise
      "Misusage error: ~
                empty list of labels in a label declaration.")
     (pristate-fix pstate))
    (pstate (print-label-declaration labels pstate)))
   (print-label-declaration-list (cdr labelss)
                                 pstate))))

Theorem: pristatep-of-print-label-declaration-list

(defthm pristatep-of-print-label-declaration-list
  (b* ((new-pstate (print-label-declaration-list labelss pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: pristate->gcc-of-print-label-declaration-list

(defthm pristate->gcc-of-print-label-declaration-list
  (b* ((?new-pstate (print-label-declaration-list labelss pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: print-label-declaration-list-of-ident-list-list-fix-labelss

(defthm print-label-declaration-list-of-ident-list-list-fix-labelss
  (equal (print-label-declaration-list (ident-list-list-fix labelss)
                                       pstate)
         (print-label-declaration-list labelss pstate)))

Theorem: print-label-declaration-list-ident-list-list-equiv-congruence-on-labelss

(defthm
 print-label-declaration-list-ident-list-list-equiv-congruence-on-labelss
 (implies
      (ident-list-list-equiv labelss labelss-equiv)
      (equal (print-label-declaration-list labelss pstate)
             (print-label-declaration-list labelss-equiv pstate)))
 :rule-classes :congruence)

Theorem: print-label-declaration-list-of-pristate-fix-pstate

(defthm print-label-declaration-list-of-pristate-fix-pstate
 (equal (print-label-declaration-list labelss (pristate-fix pstate))
        (print-label-declaration-list labelss pstate)))

Theorem: print-label-declaration-list-pristate-equiv-congruence-on-pstate

(defthm
   print-label-declaration-list-pristate-equiv-congruence-on-pstate
  (implies
       (pristate-equiv pstate pstate-equiv)
       (equal (print-label-declaration-list labelss pstate)
              (print-label-declaration-list labelss pstate-equiv)))
  :rule-classes :congruence)