		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-usuffix

Print an unsigned suffix.

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

Definitions and Theorems

Function: print-usuffix

(defun print-usuffix (usuffix pstate)
  (declare (xargs :guard (and (usuffixp usuffix)
                              (pristatep pstate))))
  (let ((__function__ 'print-usuffix))
    (declare (ignorable __function__))
    (usuffix-case usuffix
                  :locase-u (print-astring "u" pstate)
                  :upcase-u (print-astring "U" pstate))))

Theorem: pristatep-of-print-usuffix

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

Theorem: print-usuffix-of-usuffix-fix-usuffix

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

Theorem: print-usuffix-usuffix-equiv-congruence-on-usuffix

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

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

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

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

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