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