		Search-engine friendly clone of the ACL2 documentation.

Atc-pretty-printer

Pprint-const

Pretty-print a constant.

Signature
(pprint-const c) → part
Arguments: c — Guard (constp c).
Returns: part — Type (msgp part).

We cause an error when we encounter the placeholders for floating, enumeration, and character constants.

Definitions and Theorems

Function: pprint-const

(defun pprint-const (c)
 (declare (xargs :guard (constp c)))
 (let ((__function__ 'pprint-const))
  (declare (ignorable __function__))
  (const-case
   c
   :int (pprint-iconst c.get)
   :float
   (prog2$
    (raise
     "Internal error: ~
                                     floating constants not supported.")
    "")
   :enum (pprint-ident c.get)
   :char
   (prog2$
    (raise
     "Internal error: ~
                                    character constants not supported.")
    ""))))

Theorem: msgp-of-pprint-const

(defthm msgp-of-pprint-const
  (b* ((part (pprint-const c)))
    (msgp part))
  :rule-classes :rewrite)

Theorem: pprint-const-of-const-fix-c

(defthm pprint-const-of-const-fix-c
  (equal (pprint-const (const-fix c))
         (pprint-const c)))

Theorem: pprint-const-const-equiv-congruence-on-c

(defthm pprint-const-const-equiv-congruence-on-c
  (implies (const-equiv c c-equiv)
           (equal (pprint-const c)
                  (pprint-const c-equiv)))
  :rule-classes :congruence)