		Search-engine friendly clone of the ACL2 documentation.

Pretty-printer

Pprint-fundecl

Pretty-print a function declaration.

Signature
(pprint-fundecl decl level) → lines
Arguments: decl — Guard (fundeclp decl).; level — Guard (natp level).
Returns: lines — Type (msg-listp lines).

Definitions and Theorems

Function: pprint-fundecl

(defun pprint-fundecl (decl level)
 (declare (xargs :guard (and (fundeclp decl) (natp level))))
 (let ((__function__ 'pprint-fundecl))
  (declare (ignorable __function__))
  (b* (((fundecl decl) decl))
   (append
    (pprint-annotation-list decl.annotations level)
    (list
     (pprint-line
      (msg
         "function ~@0(~@1) -> ~@2 {"
         (pprint-identifier decl.name)
         (pprint-comma-separated (pprint-funparam-list decl.inputs))
         (pprint-type decl.output))
      level))
    (pprint-statement-list decl.body (1+ level))
    (list (pprint-line "}" level))))))

Theorem: msg-listp-of-pprint-fundecl

(defthm msg-listp-of-pprint-fundecl
  (b* ((lines (pprint-fundecl decl level)))
    (msg-listp lines))
  :rule-classes :rewrite)