Print a storage class specifier.
(print-stoclaspec stoclaspec pstate) → new-pstate
Function:
(defun print-stoclaspec (stoclaspec pstate) (declare (xargs :guard (and (stoclaspecp stoclaspec) (pristatep pstate)))) (let ((__function__ 'print-stoclaspec)) (declare (ignorable __function__)) (stoclaspec-case stoclaspec :typedef (print-astring "typedef" pstate) :extern (print-astring "extern" pstate) :static (print-astring "static" pstate) :threadloc (print-astring "_Thread_local" pstate) :auto (print-astring "auto" pstate) :register (print-astring "register" pstate))))
Theorem:
(defthm pristatep-of-print-stoclaspec (b* ((new-pstate (print-stoclaspec stoclaspec pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm print-stoclaspec-of-stoclaspec-fix-stoclaspec (equal (print-stoclaspec (stoclaspec-fix stoclaspec) pstate) (print-stoclaspec stoclaspec pstate)))
Theorem:
(defthm print-stoclaspec-stoclaspec-equiv-congruence-on-stoclaspec (implies (stoclaspec-equiv stoclaspec stoclaspec-equiv) (equal (print-stoclaspec stoclaspec pstate) (print-stoclaspec stoclaspec-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-stoclaspec-of-pristate-fix-pstate (equal (print-stoclaspec stoclaspec (pristate-fix pstate)) (print-stoclaspec stoclaspec pstate)))
Theorem:
(defthm print-stoclaspec-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-stoclaspec stoclaspec pstate) (print-stoclaspec stoclaspec pstate-equiv))) :rule-classes :congruence)