Print a list of one or more identifiers, separated by commas.
(print-ident-list idents pstate) → new-pstate
In our abstract syntax, ident-list is used only
in the
Function:
(defun print-ident-list (idents pstate) (declare (xargs :guard (and (ident-listp idents) (pristatep pstate)))) (declare (xargs :guard (consp idents))) (let ((__function__ 'print-ident-list)) (declare (ignorable __function__)) (b* (((unless (mbt (consp idents))) (pristate-fix pstate)) (pstate (print-ident (car idents) pstate)) ((when (endp (cdr idents))) pstate) (pstate (print-astring ", " pstate))) (print-ident-list (cdr idents) pstate))))
Theorem:
(defthm pristatep-of-print-ident-list (b* ((new-pstate (print-ident-list idents pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm print-ident-list-of-ident-list-fix-idents (equal (print-ident-list (ident-list-fix idents) pstate) (print-ident-list idents pstate)))
Theorem:
(defthm print-ident-list-ident-list-equiv-congruence-on-idents (implies (ident-list-equiv idents idents-equiv) (equal (print-ident-list idents pstate) (print-ident-list idents-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-ident-list-of-pristate-fix-pstate (equal (print-ident-list idents (pristate-fix pstate)) (print-ident-list idents pstate)))
Theorem:
(defthm print-ident-list-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-ident-list idents pstate) (print-ident-list idents pstate-equiv))) :rule-classes :congruence)