		Search-engine friendly clone of the ACL2 documentation.

Pretty-printer

Pprint-var/const-sort

Pretty-print a variable or constant sort.

Signature
(pprint-var/const-sort fps) → part
Arguments: fps — Guard (var/const-sortp fps).
Returns: part — Type (msgp part).

Nothing is printed for private, since it is the default.

A space is printed after each of the others, so that the message part returned by this fucntion can be always put in front of the rest of the function parameter.

Definitions and Theorems

Function: pprint-var/const-sort

(defun pprint-var/const-sort (fps)
  (declare (xargs :guard (var/const-sortp fps)))
  (let ((__function__ 'pprint-var/const-sort))
    (declare (ignorable __function__))
    (var/const-sort-case fps
                         :public "public "
                         :private ""
                         :constant "constant "
                         :const "const ")))

Theorem: msgp-of-pprint-var/const-sort

(defthm msgp-of-pprint-var/const-sort
  (b* ((part (pprint-var/const-sort fps)))
    (msgp part))
  :rule-classes :rewrite)

Theorem: pprint-var/const-sort-of-var/const-sort-fix-fps

(defthm pprint-var/const-sort-of-var/const-sort-fix-fps
  (equal (pprint-var/const-sort (var/const-sort-fix fps))
         (pprint-var/const-sort fps)))

Theorem: pprint-var/const-sort-var/const-sort-equiv-congruence-on-fps

(defthm pprint-var/const-sort-var/const-sort-equiv-congruence-on-fps
  (implies (var/const-sort-equiv fps fps-equiv)
           (equal (pprint-var/const-sort fps)
                  (pprint-var/const-sort fps-equiv)))
  :rule-classes :congruence)