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