		Search-engine friendly clone of the ACL2 documentation.

Atc-pretty-printer

Pprint-fun-declon

Pretty-print a function declaration.

Signature
(pprint-fun-declon declon level) → lines
Arguments: declon — Guard (fun-declonp declon).; level — Guard (natp level).
Returns: lines — Type (msg-listp lines).

Definitions and Theorems

Function: pprint-fun-declon

(defun pprint-fun-declon (declon level)
  (declare (xargs :guard (and (fun-declonp declon)
                              (natp level))))
  (let ((__function__ 'pprint-fun-declon))
    (declare (ignorable __function__))
    (b* (((fun-declon declon) declon))
      (pprint-one-line (msg "~@0 ~@1;"
                            (pprint-tyspecseq declon.tyspec)
                            (pprint-fun-declor declon.declor))
                       (lnfix level)))))

Theorem: msg-listp-of-pprint-fun-declon

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

Theorem: pprint-fun-declon-of-fun-declon-fix-declon

(defthm pprint-fun-declon-of-fun-declon-fix-declon
  (equal (pprint-fun-declon (fun-declon-fix declon)
                            level)
         (pprint-fun-declon declon level)))

Theorem: pprint-fun-declon-fun-declon-equiv-congruence-on-declon

(defthm pprint-fun-declon-fun-declon-equiv-congruence-on-declon
  (implies (fun-declon-equiv declon declon-equiv)
           (equal (pprint-fun-declon declon level)
                  (pprint-fun-declon declon-equiv level)))
  :rule-classes :congruence)

Theorem: pprint-fun-declon-of-nfix-level

(defthm pprint-fun-declon-of-nfix-level
  (equal (pprint-fun-declon declon (nfix level))
         (pprint-fun-declon declon level)))

Theorem: pprint-fun-declon-nat-equiv-congruence-on-level

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