		Search-engine friendly clone of the ACL2 documentation.

Pretty-printer

Pprint-vardecl

Pretty-print a variable declaration.

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

Definitions and Theorems

Function: pprint-vardecl

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

Theorem: msgp-of-pprint-vardecl

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

Theorem: pprint-vardecl-of-vardecl-fix-decl

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

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

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

Theorem: pprint-vardecl-of-nfix-level

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

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

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