		Search-engine friendly clone of the ACL2 documentation.

Input-execution

Eval-input-item-list

Evaluate a list of input items.

Signature
(eval-input-item-list initems intitle curve) → funargs
Arguments: initems — Guard (input-item-listp initems).; intitle — Guard (input-titlep intitle).; curve — Guard (curvep curve).
Returns: funargs — Type (funarg-list-resultp funargs).

We evaluate them one after the other, returning a corresponding list of function arguments. We stop as soon as there is an error.

Definitions and Theorems

Function: eval-input-item-list

(defun eval-input-item-list (initems intitle curve)
  (declare (xargs :guard (and (input-item-listp initems)
                              (input-titlep intitle)
                              (curvep curve))))
  (let ((__function__ 'eval-input-item-list))
    (declare (ignorable __function__))
    (b* (((when (endp initems)) nil)
         ((okf funarg)
          (eval-input-item (car initems)
                           intitle curve))
         ((okf funargs)
          (eval-input-item-list (cdr initems)
                                intitle curve)))
      (cons funarg funargs))))

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

(defthm funarg-list-resultp-of-eval-input-item-list
  (b* ((funargs (eval-input-item-list initems intitle curve)))
    (funarg-list-resultp funargs))
  :rule-classes :rewrite)

Theorem: eval-input-item-list-of-input-item-list-fix-initems

(defthm eval-input-item-list-of-input-item-list-fix-initems
  (equal (eval-input-item-list (input-item-list-fix initems)
                               intitle curve)
         (eval-input-item-list initems intitle curve)))

Theorem: eval-input-item-list-input-item-list-equiv-congruence-on-initems

(defthm
   eval-input-item-list-input-item-list-equiv-congruence-on-initems
  (implies
       (input-item-list-equiv initems initems-equiv)
       (equal (eval-input-item-list initems intitle curve)
              (eval-input-item-list initems-equiv intitle curve)))
  :rule-classes :congruence)

Theorem: eval-input-item-list-of-input-title-fix-intitle

(defthm eval-input-item-list-of-input-title-fix-intitle
  (equal (eval-input-item-list initems (input-title-fix intitle)
                               curve)
         (eval-input-item-list initems intitle curve)))

Theorem: eval-input-item-list-input-title-equiv-congruence-on-intitle

(defthm eval-input-item-list-input-title-equiv-congruence-on-intitle
  (implies
       (input-title-equiv intitle intitle-equiv)
       (equal (eval-input-item-list initems intitle curve)
              (eval-input-item-list initems intitle-equiv curve)))
  :rule-classes :congruence)

Theorem: eval-input-item-list-of-curve-fix-curve

(defthm eval-input-item-list-of-curve-fix-curve
  (equal (eval-input-item-list initems intitle (curve-fix curve))
         (eval-input-item-list initems intitle curve)))

Theorem: eval-input-item-list-curve-equiv-congruence-on-curve

(defthm eval-input-item-list-curve-equiv-congruence-on-curve
  (implies
       (curve-equiv curve curve-equiv)
       (equal (eval-input-item-list initems intitle curve)
              (eval-input-item-list initems intitle curve-equiv)))
  :rule-classes :congruence)