		Search-engine friendly clone of the ACL2 documentation.

Pretty-printer

Pprint-funparam

Pretty-print a function parameter.

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

Definitions and Theorems

Function: pprint-funparam

(defun pprint-funparam (param)
  (declare (xargs :guard (funparamp param)))
  (let ((__function__ 'pprint-funparam))
    (declare (ignorable __function__))
    (b* (((funparam param) param))
      (msg "~@0~@1: ~@2"
           (pprint-var/const-sort param.sort)
           (pprint-identifier param.name)
           (pprint-type param.type)))))

Theorem: msgp-of-pprint-funparam

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

Theorem: pprint-funparam-of-funparam-fix-param

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

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

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