		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-attrib-name

Print an attribute name.

Signature
(print-attrib-name attrname pstate) → new-pstate
Arguments: attrname — Guard (attrib-namep attrname).; pstate — Guard (pristatep pstate).
Returns: new-pstate — Type (pristatep new-pstate).

Definitions and Theorems

Function: print-attrib-name

(defun print-attrib-name (attrname pstate)
 (declare (xargs :guard (and (attrib-namep attrname)
                             (pristatep pstate))))
 (declare
  (xargs
      :guard (attrib-name-aidentp attrname (pristate->gcc pstate))))
 (let ((__function__ 'print-attrib-name))
  (declare (ignorable __function__))
  (attrib-name-case
   attrname :ident
   (print-ident attrname.unwrap pstate)
   :keyword
   (b*
    ((chars (acl2::string=>nats attrname.unwrap))
     ((unless (grammar-character-listp chars))
      (raise
       "Misusage error: ~
                          the attribute name keyword consists of ~
                          the character codes ~x0, ~
                          not all of which are allowed by the ABNF grammar."
       chars)
      (pristate-fix pstate)))
    (print-astring attrname.unwrap pstate)))))

Theorem: pristatep-of-print-attrib-name

(defthm pristatep-of-print-attrib-name
  (b* ((new-pstate (print-attrib-name attrname pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: pristate->gcc-of-print-attrib-name

(defthm pristate->gcc-of-print-attrib-name
  (b* ((?new-pstate (print-attrib-name attrname pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: print-attrib-name-of-attrib-name-fix-attrname

(defthm print-attrib-name-of-attrib-name-fix-attrname
  (equal (print-attrib-name (attrib-name-fix attrname)
                            pstate)
         (print-attrib-name attrname pstate)))

Theorem: print-attrib-name-attrib-name-equiv-congruence-on-attrname

(defthm print-attrib-name-attrib-name-equiv-congruence-on-attrname
  (implies (attrib-name-equiv attrname attrname-equiv)
           (equal (print-attrib-name attrname pstate)
                  (print-attrib-name attrname-equiv pstate)))
  :rule-classes :congruence)

Theorem: print-attrib-name-of-pristate-fix-pstate

(defthm print-attrib-name-of-pristate-fix-pstate
  (equal (print-attrib-name attrname (pristate-fix pstate))
         (print-attrib-name attrname pstate)))

Theorem: print-attrib-name-pristate-equiv-congruence-on-pstate

(defthm print-attrib-name-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-attrib-name attrname pstate)
                  (print-attrib-name attrname pstate-equiv)))
  :rule-classes :congruence)