Cause an error if a value is not a print specifier.
(ensure-is-print-specifier x description error-erp error-val ctx state) → (mv erp val state)
Function:
(defun ensure-is-print-specifier (x description error-erp error-val ctx state) (declare (xargs :stobjs (state))) (declare (xargs :guard (msgp description))) (b* (((unless (print-specifier-p x)) (er-soft+ ctx error-erp error-val "~@0 must be a print specifier. See :DOC APT::PRINT-SPECIFIER." description))) (value nil)))
Theorem:
(defthm return-type-of-ensure-is-print-specifier.erp (b* (((mv ?erp ?val acl2::?state) (ensure-is-print-specifier x description error-erp error-val ctx state))) (implies erp (equal erp error-erp))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-ensure-is-print-specifier.val (b* (((mv ?erp ?val acl2::?state) (ensure-is-print-specifier x description error-erp error-val ctx state))) (and (implies erp (equal val error-val)) (implies (and (not erp) error-erp) (not val)))) :rule-classes :rewrite)