		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-stringlit

Print a string literal.

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

Definitions and Theorems

Function: print-stringlit

(defun print-stringlit (stringlit pstate)
  (declare (xargs :guard (and (stringlitp stringlit)
                              (pristatep pstate))))
  (let ((__function__ 'print-stringlit))
    (declare (ignorable __function__))
    (b* (((stringlit stringlit) stringlit)
         (pstate (print-eprefix-option stringlit.prefix? pstate))
         (pstate (print-astring "\"" pstate))
         (pstate (print-s-char-list stringlit.schars pstate))
         (pstate (print-astring "\"" pstate)))
      pstate)))

Theorem: pristatep-of-print-stringlit

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

Theorem: print-stringlit-of-stringlit-fix-stringlit

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

Theorem: print-stringlit-stringlit-equiv-congruence-on-stringlit

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

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

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

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

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