		Search-engine friendly clone of the ACL2 documentation.

Atj-java-pretty-printer

Print-jparam-list

Pretty-print a formal parameter list.

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

Definitions and Theorems

Function: print-jparam-list

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

Theorem: msg-listp-of-print-jparam-list

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