Check an output item.
(check-output-item outitem env) → type
We check the underlying output expression, returning its type.
Function:
(defun check-output-item (outitem env) (declare (xargs :guard (and (output-itemp outitem) (senvp env)))) (let ((__function__ 'check-output-item)) (declare (ignorable __function__)) (check-output-expression (output-item->get outitem) env)))
Theorem:
(defthm type-resultp-of-check-output-item (b* ((type (check-output-item outitem env))) (type-resultp type)) :rule-classes :rewrite)
Theorem:
(defthm check-output-item-of-output-item-fix-outitem (equal (check-output-item (output-item-fix outitem) env) (check-output-item outitem env)))
Theorem:
(defthm check-output-item-output-item-equiv-congruence-on-outitem (implies (output-item-equiv outitem outitem-equiv) (equal (check-output-item outitem env) (check-output-item outitem-equiv env))) :rule-classes :congruence)
Theorem:
(defthm check-output-item-of-senv-fix-env (equal (check-output-item outitem (senv-fix env)) (check-output-item outitem env)))
Theorem:
(defthm check-output-item-senv-equiv-congruence-on-env (implies (senv-equiv env env-equiv) (equal (check-output-item outitem env) (check-output-item outitem env-equiv))) :rule-classes :congruence)