Print an attribute specifier.
(print-attrib-spec attrspec pstate) → new-pstate
Function:
(defun print-attrib-spec (attrspec pstate) (declare (xargs :guard (and (attrib-specp attrspec) (pristatep pstate)))) (let ((__function__ 'print-attrib-spec)) (declare (ignorable __function__)) (b* ((pstate (print-astring "__attribute__ ((" pstate)) (attrs (attrib-spec->attribs attrspec)) (pstate (if (consp attrs) (print-attrib-list attrs pstate) pstate)) (pstate (print-astring "))" pstate))) pstate)))
Theorem:
(defthm pristatep-of-print-attrib-spec (b* ((new-pstate (print-attrib-spec attrspec pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm print-attrib-spec-of-attrib-spec-fix-attrspec (equal (print-attrib-spec (attrib-spec-fix attrspec) pstate) (print-attrib-spec attrspec pstate)))
Theorem:
(defthm print-attrib-spec-attrib-spec-equiv-congruence-on-attrspec (implies (attrib-spec-equiv attrspec attrspec-equiv) (equal (print-attrib-spec attrspec pstate) (print-attrib-spec attrspec-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-attrib-spec-of-pristate-fix-pstate (equal (print-attrib-spec attrspec (pristate-fix pstate)) (print-attrib-spec attrspec pstate)))
Theorem:
(defthm print-attrib-spec-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-attrib-spec attrspec pstate) (print-attrib-spec attrspec pstate-equiv))) :rule-classes :congruence)