		Search-engine friendly clone of the ACL2 documentation.

Pretty-printer

Pprint-compdecl-list

Pretty-print a list of struct component declarations.

Signature
(pprint-compdecl-list decls level) → lines
Arguments: decls — Guard (compdecl-listp decls).; level — Guard (natp level).
Returns: lines — Type (msg-listp lines).

Definitions and Theorems

Function: pprint-compdecl-list

(defun pprint-compdecl-list (decls level)
 (declare (xargs :guard (and (compdecl-listp decls)
                             (natp level))))
 (let ((__function__ 'pprint-compdecl-list))
  (declare (ignorable __function__))
  (cond
   ((endp decls) nil)
   ((endp (cdr decls))
    (list (pprint-line (pprint-compdecl (car decls))
                       level)))
   (t
    (append
       (list (pprint-line (msg "~@0," (pprint-compdecl (car decls)))
                          level))
       (pprint-compdecl-list (cdr decls)
                             level))))))

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

(defthm msg-listp-of-pprint-compdecl-list
  (b* ((lines (pprint-compdecl-list decls level)))
    (msg-listp lines))
  :rule-classes :rewrite)