		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-bexprefix

Print a binary exponent prefix.

Signature
(print-bexprefix prefix pstate) → new-pstate
Arguments: prefix — Guard (bexprefixp prefix).; pstate — Guard (pristatep pstate).
Returns: new-pstate — Type (pristatep new-pstate).

Definitions and Theorems

Function: print-bexprefix

(defun print-bexprefix (prefix pstate)
  (declare (xargs :guard (and (bexprefixp prefix)
                              (pristatep pstate))))
  (let ((__function__ 'print-bexprefix))
    (declare (ignorable __function__))
    (bexprefix-case prefix
                    :locase-p (print-astring "p" pstate)
                    :upcase-p (print-astring "P" pstate))))

Theorem: pristatep-of-print-bexprefix

(defthm pristatep-of-print-bexprefix
  (b* ((new-pstate (print-bexprefix prefix pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: pristate->gcc-of-print-bexprefix

(defthm pristate->gcc-of-print-bexprefix
  (b* ((?new-pstate (print-bexprefix prefix pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: print-bexprefix-of-bexprefix-fix-prefix

(defthm print-bexprefix-of-bexprefix-fix-prefix
  (equal (print-bexprefix (bexprefix-fix prefix)
                          pstate)
         (print-bexprefix prefix pstate)))

Theorem: print-bexprefix-bexprefix-equiv-congruence-on-prefix

(defthm print-bexprefix-bexprefix-equiv-congruence-on-prefix
  (implies (bexprefix-equiv prefix prefix-equiv)
           (equal (print-bexprefix prefix pstate)
                  (print-bexprefix prefix-equiv pstate)))
  :rule-classes :congruence)

Theorem: print-bexprefix-of-pristate-fix-pstate

(defthm print-bexprefix-of-pristate-fix-pstate
  (equal (print-bexprefix prefix (pristate-fix pstate))
         (print-bexprefix prefix pstate)))

Theorem: print-bexprefix-pristate-equiv-congruence-on-pstate

(defthm print-bexprefix-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-bexprefix prefix pstate)
                  (print-bexprefix prefix pstate-equiv)))
  :rule-classes :congruence)