Print a type qualifier.
(print-type-qual tyqual pstate) → new-pstate
Function:
(defun print-type-qual (tyqual pstate) (declare (xargs :guard (and (type-qualp tyqual) (pristatep pstate)))) (let ((__function__ 'print-type-qual)) (declare (ignorable __function__)) (type-qual-case tyqual :const (print-astring "const" pstate) :restrict (keyword-uscores-case tyqual.uscores :none (print-astring "restrict" pstate) :start (print-astring "__restrict" pstate) :both (print-astring "__restrict__" pstate)) :volatile (print-astring "volatile" pstate) :atomic (print-astring "_Atomic" pstate))))
Theorem:
(defthm pristatep-of-print-type-qual (b* ((new-pstate (print-type-qual tyqual pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm print-type-qual-of-type-qual-fix-tyqual (equal (print-type-qual (type-qual-fix tyqual) pstate) (print-type-qual tyqual pstate)))
Theorem:
(defthm print-type-qual-type-qual-equiv-congruence-on-tyqual (implies (type-qual-equiv tyqual tyqual-equiv) (equal (print-type-qual tyqual pstate) (print-type-qual tyqual-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-type-qual-of-pristate-fix-pstate (equal (print-type-qual tyqual (pristate-fix pstate)) (print-type-qual tyqual pstate)))
Theorem:
(defthm print-type-qual-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-type-qual tyqual pstate) (print-type-qual tyqual pstate-equiv))) :rule-classes :congruence)