		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-label-declaration

Print a label declaration consisting of one or more labels.

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

Definitions and Theorems

Function: print-label-declaration

(defun print-label-declaration (labels pstate)
 (declare (xargs :guard (and (ident-listp labels)
                             (pristatep pstate))))
 (declare
  (xargs
   :guard (and (consp labels)
               (ident-list-aidentp labels (pristate->gcc pstate)))))
 (let ((__function__ 'print-label-declaration))
   (declare (ignorable __function__))
   (b* ((pstate (print-indent pstate))
        (pstate (print-astring "__label__ " pstate))
        (pstate (print-ident-list labels pstate))
        (pstate (print-astring ";" pstate))
        (pstate (print-new-line pstate)))
     pstate)))

Theorem: pristatep-of-print-label-declaration

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

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

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

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

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

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

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

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

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

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

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