Pretty-print an optional integer type suffix.
(print-optional-integer-type-suffix l/l?) → part
Function:
(defun print-optional-integer-type-suffix (l/l?) (declare (xargs :guard (optional-integer-type-suffix-p l/l?))) (let ((__function__ 'print-optional-integer-type-suffix)) (declare (ignorable __function__)) (optional-integer-type-suffix-case l/l? :none "" :lowercase "l" :uppercase "L")))
Theorem:
(defthm msgp-of-print-optional-integer-type-suffix (b* ((part (print-optional-integer-type-suffix l/l?))) (msgp part)) :rule-classes :rewrite)
Theorem:
(defthm print-optional-integer-type-suffix-of-optional-integer-type-suffix-fix-l/l? (equal (print-optional-integer-type-suffix (optional-integer-type-suffix-fix l/l?)) (print-optional-integer-type-suffix l/l?)))
Theorem:
(defthm print-optional-integer-type-suffix-optional-integer-type-suffix-equiv-congruence-on-l/l? (implies (optional-integer-type-suffix-equiv l/l? l/l?-equiv) (equal (print-optional-integer-type-suffix l/l?) (print-optional-integer-type-suffix l/l?-equiv))) :rule-classes :congruence)