		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-hprefix

Print a hexadecimal prefix.

Signature
(print-hprefix hprefix pstate) → new-pstate
Arguments: hprefix — Guard (hprefixp hprefix).; pstate — Guard (pristatep pstate).
Returns: new-pstate — Type (pristatep new-pstate).

Definitions and Theorems

Function: print-hprefix

(defun print-hprefix (hprefix pstate)
  (declare (xargs :guard (and (hprefixp hprefix)
                              (pristatep pstate))))
  (let ((__function__ 'print-hprefix))
    (declare (ignorable __function__))
    (hprefix-case hprefix
                  :locase-0x (print-astring "0x" pstate)
                  :upcase-0x (print-astring "0X" pstate))))

Theorem: pristatep-of-print-hprefix

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

Theorem: print-hprefix-of-hprefix-fix-hprefix

(defthm print-hprefix-of-hprefix-fix-hprefix
  (equal (print-hprefix (hprefix-fix hprefix)
                        pstate)
         (print-hprefix hprefix pstate)))

Theorem: print-hprefix-hprefix-equiv-congruence-on-hprefix

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

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

(defthm print-hprefix-of-pristate-fix-pstate
  (equal (print-hprefix hprefix (pristate-fix pstate))
         (print-hprefix hprefix pstate)))

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

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