		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-oct-escape

Print an octal escape.

Signature
(print-oct-escape esc pstate) → new-pstate
Arguments: esc — Guard (oct-escapep esc).; pstate — Guard (pristatep pstate).
Returns: new-pstate — Type (pristatep new-pstate).

Definitions and Theorems

Function: print-oct-escape

(defun print-oct-escape (esc pstate)
 (declare (xargs :guard (and (oct-escapep esc)
                             (pristatep pstate))))
 (let ((__function__ 'print-oct-escape))
  (declare (ignorable __function__))
  (b*
   ((pstate (print-astring "\\" pstate))
    (pstate
       (oct-escape-case
            esc :one
            (print-oct-digit-achar esc.digit pstate)
            :two
            (b* ((pstate (print-oct-digit-achar esc.digit1 pstate))
                 (pstate (print-oct-digit-achar esc.digit2 pstate)))
              pstate)
            :three
            (b* ((pstate (print-oct-digit-achar esc.digit1 pstate))
                 (pstate (print-oct-digit-achar esc.digit2 pstate))
                 (pstate (print-oct-digit-achar esc.digit3 pstate)))
              pstate))))
   pstate)))

Theorem: pristatep-of-print-oct-escape

(defthm pristatep-of-print-oct-escape
  (b* ((new-pstate (print-oct-escape esc pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: print-oct-escape-of-oct-escape-fix-esc

(defthm print-oct-escape-of-oct-escape-fix-esc
  (equal (print-oct-escape (oct-escape-fix esc)
                           pstate)
         (print-oct-escape esc pstate)))

Theorem: print-oct-escape-oct-escape-equiv-congruence-on-esc

(defthm print-oct-escape-oct-escape-equiv-congruence-on-esc
  (implies (oct-escape-equiv esc esc-equiv)
           (equal (print-oct-escape esc pstate)
                  (print-oct-escape esc-equiv pstate)))
  :rule-classes :congruence)

Theorem: print-oct-escape-of-pristate-fix-pstate

(defthm print-oct-escape-of-pristate-fix-pstate
  (equal (print-oct-escape esc (pristate-fix pstate))
         (print-oct-escape esc pstate)))

Theorem: print-oct-escape-pristate-equiv-congruence-on-pstate

(defthm print-oct-escape-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-oct-escape esc pstate)
                  (print-oct-escape esc pstate-equiv)))
  :rule-classes :congruence)