Print an optional sign.
(print-sign-option sign? pstate) → new-pstate
If there is no sign, we print nothing.
Function:
(defun print-sign-option (sign? pstate) (declare (xargs :guard (and (sign-optionp sign?) (pristatep pstate)))) (let ((__function__ 'print-sign-option)) (declare (ignorable __function__)) (sign-option-case sign? :some (print-sign sign?.val pstate) :none (pristate-fix pstate))))
Theorem:
(defthm pristatep-of-print-sign-option (b* ((new-pstate (print-sign-option sign? pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm print-sign-option-of-sign-option-fix-sign? (equal (print-sign-option (sign-option-fix sign?) pstate) (print-sign-option sign? pstate)))
Theorem:
(defthm print-sign-option-sign-option-equiv-congruence-on-sign? (implies (sign-option-equiv sign? sign?-equiv) (equal (print-sign-option sign? pstate) (print-sign-option sign?-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-sign-option-of-pristate-fix-pstate (equal (print-sign-option sign? (pristate-fix pstate)) (print-sign-option sign? pstate)))
Theorem:
(defthm print-sign-option-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-sign-option sign? pstate) (print-sign-option sign? pstate-equiv))) :rule-classes :congruence)