		Search-engine friendly clone of the ACL2 documentation.

Pretty-printer

Pprint-group-literal

Pretty-print a group literal.

Signature
(pprint-group-literal lit) → part
Arguments: lit — Guard (group-literalp lit).
Returns: part — Type (msgp part).

Definitions and Theorems

Function: pprint-group-literal

(defun pprint-group-literal (lit)
 (declare (xargs :guard (group-literalp lit)))
 (let ((__function__ 'pprint-group-literal))
   (declare (ignorable __function__))
   (group-literal-case lit
                       :affine (msg "(~@0, ~@1)group"
                                    (pprint-coordinate lit.x)
                                    (pprint-coordinate lit.y))
                       :product (msg "~@0group"
                                     (pprint-natural lit.factor)))))

Theorem: msgp-of-pprint-group-literal

(defthm msgp-of-pprint-group-literal
  (b* ((part (pprint-group-literal lit)))
    (msgp part))
  :rule-classes :rewrite)

Theorem: pprint-group-literal-of-group-literal-fix-lit

(defthm pprint-group-literal-of-group-literal-fix-lit
  (equal (pprint-group-literal (group-literal-fix lit))
         (pprint-group-literal lit)))

Theorem: pprint-group-literal-group-literal-equiv-congruence-on-lit

(defthm pprint-group-literal-group-literal-equiv-congruence-on-lit
  (implies (group-literal-equiv lit lit-equiv)
           (equal (pprint-group-literal lit)
                  (pprint-group-literal lit-equiv)))
  :rule-classes :congruence)