		Search-engine friendly clone of the ACL2 documentation.

Input-execution

Eval-input-section

Evaluate an input section.

Signature
(eval-input-section insec curve) → funargs
Arguments: insec — Guard (input-sectionp insec).; curve — Guard (curvep curve).
Returns: funargs — Type (funarg-list-resultp funargs).

We evaluate its items, using the input title as the sort.

Definitions and Theorems

Function: eval-input-section

(defun eval-input-section (insec curve)
  (declare (xargs :guard (and (input-sectionp insec)
                              (curvep curve))))
  (let ((__function__ 'eval-input-section))
    (declare (ignorable __function__))
    (eval-input-item-list (input-section->items insec)
                          (input-section->title insec)
                          curve)))

Theorem: funarg-list-resultp-of-eval-input-section

(defthm funarg-list-resultp-of-eval-input-section
  (b* ((funargs (eval-input-section insec curve)))
    (funarg-list-resultp funargs))
  :rule-classes :rewrite)

Theorem: eval-input-section-of-input-section-fix-insec

(defthm eval-input-section-of-input-section-fix-insec
  (equal (eval-input-section (input-section-fix insec)
                             curve)
         (eval-input-section insec curve)))

Theorem: eval-input-section-input-section-equiv-congruence-on-insec

(defthm eval-input-section-input-section-equiv-congruence-on-insec
  (implies (input-section-equiv insec insec-equiv)
           (equal (eval-input-section insec curve)
                  (eval-input-section insec-equiv curve)))
  :rule-classes :congruence)

Theorem: eval-input-section-of-curve-fix-curve

(defthm eval-input-section-of-curve-fix-curve
  (equal (eval-input-section insec (curve-fix curve))
         (eval-input-section insec curve)))

Theorem: eval-input-section-curve-equiv-congruence-on-curve

(defthm eval-input-section-curve-equiv-congruence-on-curve
  (implies (curve-equiv curve curve-equiv)
           (equal (eval-input-section insec curve)
                  (eval-input-section insec curve-equiv)))
  :rule-classes :congruence)