		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-eprefix

Print an encoding prefix.

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

Definitions and Theorems

Function: print-eprefix

(defun print-eprefix (eprefix pstate)
  (declare (xargs :guard (and (eprefixp eprefix)
                              (pristatep pstate))))
  (let ((__function__ 'print-eprefix))
    (declare (ignorable __function__))
    (eprefix-case eprefix
                  :locase-u8 (print-astring "u8" pstate)
                  :locase-u (print-astring "u" pstate)
                  :upcase-u (print-astring "U" pstate)
                  :upcase-l (print-astring "L" pstate))))

Theorem: pristatep-of-print-eprefix

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

Theorem: print-eprefix-of-eprefix-fix-eprefix

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

Theorem: print-eprefix-eprefix-equiv-congruence-on-eprefix

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

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

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

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

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