		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-lsuffix

Print a length suffix.

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

Definitions and Theorems

Function: print-lsuffix

(defun print-lsuffix (lsuffix pstate)
  (declare (xargs :guard (and (lsuffixp lsuffix)
                              (pristatep pstate))))
  (let ((__function__ 'print-lsuffix))
    (declare (ignorable __function__))
    (lsuffix-case lsuffix
                  :locase-l (print-astring "l" pstate)
                  :upcase-l (print-astring "L" pstate)
                  :locase-ll (print-astring "ll" pstate)
                  :upcase-ll (print-astring "LL" pstate))))

Theorem: pristatep-of-print-lsuffix

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

Theorem: print-lsuffix-of-lsuffix-fix-lsuffix

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

Theorem: print-lsuffix-lsuffix-equiv-congruence-on-lsuffix

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

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

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

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

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