		Search-engine friendly clone of the ACL2 documentation.

Pretty-printer

Pprint-constdecl

Pretty-print a constant declaration.

Signature
(pprint-constdecl decl level) → line
Arguments: decl — Guard (constdeclp decl).; level — Guard (natp level).
Returns: line — Type (msgp line).

Definitions and Theorems

Function: pprint-constdecl

(defun pprint-constdecl (decl level)
 (declare (xargs :guard (and (constdeclp decl) (natp level))))
 (let ((__function__ 'pprint-constdecl))
  (declare (ignorable __function__))
  (b* (((constdecl decl) decl))
   (pprint-line (msg "const ~@0: ~@1 = ~@2;"
                     (pprint-identifier decl.name)
                     (pprint-type decl.type)
                     (pprint-expression decl.init (expr-grade-top)))
                level))))

Theorem: msgp-of-pprint-constdecl

(defthm msgp-of-pprint-constdecl
  (b* ((line (pprint-constdecl decl level)))
    (msgp line))
  :rule-classes :rewrite)

Theorem: pprint-constdecl-of-constdecl-fix-decl

(defthm pprint-constdecl-of-constdecl-fix-decl
  (equal (pprint-constdecl (constdecl-fix decl)
                           level)
         (pprint-constdecl decl level)))

Theorem: pprint-constdecl-constdecl-equiv-congruence-on-decl

(defthm pprint-constdecl-constdecl-equiv-congruence-on-decl
  (implies (constdecl-equiv decl decl-equiv)
           (equal (pprint-constdecl decl level)
                  (pprint-constdecl decl-equiv level)))
  :rule-classes :congruence)

Theorem: pprint-constdecl-of-nfix-level

(defthm pprint-constdecl-of-nfix-level
  (equal (pprint-constdecl decl (nfix level))
         (pprint-constdecl decl level)))

Theorem: pprint-constdecl-nat-equiv-congruence-on-level

(defthm pprint-constdecl-nat-equiv-congruence-on-level
  (implies (acl2::nat-equiv level level-equiv)
           (equal (pprint-constdecl decl level)
                  (pprint-constdecl decl level-equiv)))
  :rule-classes :congruence)