		Search-engine friendly clone of the ACL2 documentation.

Pretty-printer

Pprint-programdecl

Pretty-print a program.

Signature
(pprint-programdecl pdecl) → lines
Arguments: pdecl — Guard (programdeclp pdecl).
Returns: lines — Type (msg-listp lines).

Definitions and Theorems

Function: pprint-programdecl

(defun pprint-programdecl (pdecl)
 (declare (xargs :guard (programdeclp pdecl)))
 (let ((__function__ 'pprint-programdecl))
  (declare (ignorable __function__))
  (cons
       (pprint-line (msg "program ~@0 {"
                         (pprint-programid (programdecl->id pdecl)))
                    0)
       (append (pprint-topdecl-list (programdecl->items pdecl))
               (list (pprint-line (msg "}") 0))))))

Theorem: msg-listp-of-pprint-programdecl

(defthm msg-listp-of-pprint-programdecl
  (b* ((lines (pprint-programdecl pdecl)))
    (msg-listp lines))
  :rule-classes :rewrite)

Theorem: pprint-programdecl-of-programdecl-fix-pdecl

(defthm pprint-programdecl-of-programdecl-fix-pdecl
  (equal (pprint-programdecl (programdecl-fix pdecl))
         (pprint-programdecl pdecl)))

Theorem: pprint-programdecl-programdecl-equiv-congruence-on-pdecl

(defthm pprint-programdecl-programdecl-equiv-congruence-on-pdecl
  (implies (programdecl-equiv pdecl pdecl-equiv)
           (equal (pprint-programdecl pdecl)
                  (pprint-programdecl pdecl-equiv)))
  :rule-classes :congruence)