		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-isuffix

Print an integer suffix.

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

Definitions and Theorems

Function: print-isuffix

(defun print-isuffix (isuffix pstate)
  (declare (xargs :guard (and (isuffixp isuffix)
                              (pristatep pstate))))
  (let ((__function__ 'print-isuffix))
    (declare (ignorable __function__))
    (isuffix-case
         isuffix :u
         (print-usuffix isuffix.unsigned pstate)
         :l (print-lsuffix isuffix.length pstate)
         :ul
         (b* ((pstate (print-usuffix isuffix.unsigned pstate))
              (pstate (print-lsuffix isuffix.length pstate)))
           pstate)
         :lu
         (b* ((pstate (print-lsuffix isuffix.length pstate))
              (pstate (print-usuffix isuffix.unsigned pstate)))
           pstate))))

Theorem: pristatep-of-print-isuffix

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

Theorem: print-isuffix-of-isuffix-fix-isuffix

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

Theorem: print-isuffix-isuffix-equiv-congruence-on-isuffix

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

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

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

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

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