		Search-engine friendly clone of the ACL2 documentation.

Atc-pretty-printer

Pprint-param-declon-list

Pretty-print a list of parameter declarations.

Signature
(pprint-param-declon-list params) → parts
Arguments: params — Guard (param-declon-listp params).
Returns: parts — Type (msg-listp parts).

Definitions and Theorems

Function: pprint-param-declon-list

(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: msg-listp-of-pprint-param-declon-list

(defthm msg-listp-of-pprint-param-declon-list
  (b* ((parts (pprint-param-declon-list params)))
    (msg-listp parts))
  :rule-classes :rewrite)

Theorem: pprint-param-declon-list-of-param-declon-list-fix-params

(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: pprint-param-declon-list-param-declon-list-equiv-congruence-on-params

(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)