		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-cconst

Print a character constant.

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

We ensure that there is at least one character or escape sequence.

Definitions and Theorems

Function: print-cconst

(defun print-cconst (cconst pstate)
 (declare (xargs :guard (and (cconstp cconst)
                             (pristatep pstate))))
 (let ((__function__ 'print-cconst))
  (declare (ignorable __function__))
  (b*
   (((cconst cconst) cconst)
    (pstate (print-cprefix-option cconst.prefix? pstate))
    (pstate (print-astring "'" pstate))
    ((unless cconst.cchars)
     (raise
      "Misusage error: ~
                the character constant has no characters or escape sequences.")
     pstate)
    (pstate (print-c-char-list cconst.cchars pstate))
    (pstate (print-astring "'" pstate)))
   pstate)))

Theorem: pristatep-of-print-cconst

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

Theorem: print-cconst-of-cconst-fix-cconst

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

Theorem: print-cconst-cconst-equiv-congruence-on-cconst

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

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

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

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

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