		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-sign

Print a sign.

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

Definitions and Theorems

Function: print-sign

(defun print-sign (sign pstate)
  (declare (xargs :guard (and (signp sign) (pristatep pstate))))
  (let ((__function__ 'print-sign))
    (declare (ignorable __function__))
    (sign-case sign
               :plus (print-astring "+" pstate)
               :minus (print-astring "-" pstate))))

Theorem: pristatep-of-print-sign

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

Theorem: print-sign-of-sign-fix-sign

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

Theorem: print-sign-sign-equiv-congruence-on-sign

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

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

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

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

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