Evaluate an output item.
(eval-output-item outitem curve) → val
Function:
(defun eval-output-item (outitem curve) (declare (xargs :guard (and (output-itemp outitem) (curvep curve)))) (let ((__function__ 'eval-output-item)) (declare (ignorable __function__)) (eval-output-expression (output-item->get outitem) curve)))
Theorem:
(defthm value-resultp-of-eval-output-item (b* ((val (eval-output-item outitem curve))) (value-resultp val)) :rule-classes :rewrite)
Theorem:
(defthm eval-output-item-of-output-item-fix-outitem (equal (eval-output-item (output-item-fix outitem) curve) (eval-output-item outitem curve)))
Theorem:
(defthm eval-output-item-output-item-equiv-congruence-on-outitem (implies (output-item-equiv outitem outitem-equiv) (equal (eval-output-item outitem curve) (eval-output-item outitem-equiv curve))) :rule-classes :congruence)
Theorem:
(defthm eval-output-item-of-curve-fix-curve (equal (eval-output-item outitem (curve-fix curve)) (eval-output-item outitem curve)))
Theorem:
(defthm eval-output-item-curve-equiv-congruence-on-curve (implies (curve-equiv curve curve-equiv) (equal (eval-output-item outitem curve) (eval-output-item outitem curve-equiv))) :rule-classes :congruence)