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