Print a list of one or more type qualifiers, separated by spaces.
(print-type-qual-list tyquals pstate) → new-pstate
Function:
(defun print-type-qual-list (tyquals pstate) (declare (xargs :guard (and (type-qual-listp tyquals) (pristatep pstate)))) (declare (xargs :guard (consp tyquals))) (let ((__function__ 'print-type-qual-list)) (declare (ignorable __function__)) (b* (((unless (mbt (consp tyquals))) (pristate-fix pstate)) (pstate (print-type-qual (car tyquals) pstate)) ((when (endp (cdr tyquals))) pstate) (pstate (print-astring " " pstate))) (print-type-qual-list (cdr tyquals) pstate))))
Theorem:
(defthm pristatep-of-print-type-qual-list (b* ((new-pstate (print-type-qual-list tyquals pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm print-type-qual-list-of-type-qual-list-fix-tyquals (equal (print-type-qual-list (type-qual-list-fix tyquals) pstate) (print-type-qual-list tyquals pstate)))
Theorem:
(defthm print-type-qual-list-type-qual-list-equiv-congruence-on-tyquals (implies (type-qual-list-equiv tyquals tyquals-equiv) (equal (print-type-qual-list tyquals pstate) (print-type-qual-list tyquals-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-type-qual-list-of-pristate-fix-pstate (equal (print-type-qual-list tyquals (pristate-fix pstate)) (print-type-qual-list tyquals pstate)))
Theorem:
(defthm print-type-qual-list-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-type-qual-list tyquals pstate) (print-type-qual-list tyquals pstate-equiv))) :rule-classes :congruence)