Pretty-print a list of identifiers.
(pprint-ident-list ids) → parts
Function:
(defun pprint-ident-list (ids) (declare (xargs :guard (ident-listp ids))) (let ((__function__ 'pprint-ident-list)) (declare (ignorable __function__)) (cond ((endp ids) nil) (t (cons (pprint-ident (car ids)) (pprint-ident-list (cdr ids)))))))
Theorem:
(defthm msg-listp-of-pprint-ident-list (b* ((parts (pprint-ident-list ids))) (msg-listp parts)) :rule-classes :rewrite)
Theorem:
(defthm pprint-ident-list-of-ident-list-fix-ids (equal (pprint-ident-list (ident-list-fix ids)) (pprint-ident-list ids)))
Theorem:
(defthm pprint-ident-list-ident-list-equiv-congruence-on-ids (implies (ident-list-equiv ids ids-equiv) (equal (pprint-ident-list ids) (pprint-ident-list ids-equiv))) :rule-classes :congruence)