		Search-engine friendly clone of the ACL2 documentation.

Pretty-printer

Pprint-funparam-list

Pretty-print a list of function parameters.

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

Definitions and Theorems

Function: pprint-funparam-list

(defun pprint-funparam-list (params)
  (declare (xargs :guard (funparam-listp params)))
  (let ((__function__ 'pprint-funparam-list))
    (declare (ignorable __function__))
    (cond ((endp params) nil)
          (t (cons (pprint-funparam (car params))
                   (pprint-funparam-list (cdr params)))))))

Theorem: msg-listp-of-pprint-funparam-list

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

Theorem: pprint-funparam-list-of-funparam-list-fix-params

(defthm pprint-funparam-list-of-funparam-list-fix-params
  (equal (pprint-funparam-list (funparam-list-fix params))
         (pprint-funparam-list params)))

Theorem: pprint-funparam-list-funparam-list-equiv-congruence-on-params

(defthm
      pprint-funparam-list-funparam-list-equiv-congruence-on-params
  (implies (funparam-list-equiv params params-equiv)
           (equal (pprint-funparam-list params)
                  (pprint-funparam-list params-equiv)))
  :rule-classes :congruence)