		Search-engine friendly clone of the ACL2 documentation.

Pretty-printer

Pprint-boolean

Pretty-print a boolean.

Signature
(pprint-boolean bool) → part
Arguments: bool — Guard (booleanp bool).
Returns: part — Type (msgp part).

Definitions and Theorems

Function: pprint-boolean

(defun pprint-boolean (bool)
  (declare (xargs :guard (booleanp bool)))
  (let ((__function__ 'pprint-boolean))
    (declare (ignorable __function__))
    (if bool "true" "false")))

Theorem: msgp-of-pprint-boolean

(defthm msgp-of-pprint-boolean
  (b* ((part (pprint-boolean bool)))
    (msgp part))
  :rule-classes :rewrite)

Theorem: pprint-boolean-of-bool-fix-bool

(defthm pprint-boolean-of-bool-fix-bool
  (equal (pprint-boolean (acl2::bool-fix bool))
         (pprint-boolean bool)))

Theorem: pprint-boolean-iff-congruence-on-bool

(defthm pprint-boolean-iff-congruence-on-bool
  (implies (iff bool bool-equiv)
           (equal (pprint-boolean bool)
                  (pprint-boolean bool-equiv)))
  :rule-classes :congruence)