		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-simple-escape

Print a simple escape.

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

Definitions and Theorems

Function: print-simple-escape

(defun print-simple-escape (esc pstate)
  (declare (xargs :guard (and (simple-escapep esc)
                              (pristatep pstate))))
  (let ((__function__ 'print-simple-escape))
    (declare (ignorable __function__))
    (simple-escape-case esc
                        :squote (print-astring "\\'" pstate)
                        :dquote (print-astring "\\\"" pstate)
                        :qmark (print-astring "\\?" pstate)
                        :bslash (print-astring "\\\\" pstate)
                        :a (print-astring "\\a" pstate)
                        :b (print-astring "\\b" pstate)
                        :f (print-astring "\\f" pstate)
                        :n (print-astring "\\n" pstate)
                        :r (print-astring "\\r" pstate)
                        :t (print-astring "\\t" pstate)
                        :v (print-astring "\\v" pstate)
                        :percent (print-astring "\\%" pstate))))

Theorem: pristatep-of-print-simple-escape

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

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

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

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

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

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

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

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

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