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