		Search-engine friendly clone of the ACL2 documentation.

Atc-pretty-printer

Pprint-param-declon

Pretty-print a parameter declaration.

Signature
(pprint-param-declon param) → part
Arguments: param — Guard (param-declonp param).
Returns: part — Type (msgp part).

Definitions and Theorems

Function: pprint-param-declon

(defun pprint-param-declon (param)
  (declare (xargs :guard (param-declonp param)))
  (let ((__function__ 'pprint-param-declon))
    (declare (ignorable __function__))
    (b* (((param-declon param) param))
      (msg "~@0 ~@1"
           (pprint-tyspecseq param.tyspec)
           (pprint-obj-declor param.declor)))))

Theorem: msgp-of-pprint-param-declon

(defthm msgp-of-pprint-param-declon
  (b* ((part (pprint-param-declon param)))
    (msgp part))
  :rule-classes :rewrite)

Theorem: pprint-param-declon-of-param-declon-fix-param

(defthm pprint-param-declon-of-param-declon-fix-param
  (equal (pprint-param-declon (param-declon-fix param))
         (pprint-param-declon param)))

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

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