		Search-engine friendly clone of the ACL2 documentation.

Atj-input-processing

Atj-process-test-inputs

Lift atj-process-test-input to lists.

Signature
(atj-process-test-inputs inputs types fn call deep$ guards$ ctx state) → (mv erp test-inputs state)
Arguments: inputs — Guard (pseudo-term-listp inputs).; types — Guard (atj-type-listp types).; fn — Just for error messages.
Guard (symbolp fn).; call — Just for error messages.
Guard (pseudo-termp call).; deep$ — Guard (booleanp deep$).; guards$ — Guard (booleanp guards$).; ctx — Guard (ctxp ctx).
Returns: test-inputs — Type (atj-test-value-listp test-inputs).

This is used to process all the inputs of a test.

Definitions and Theorems

Function: atj-process-test-inputs

(defun atj-process-test-inputs
       (inputs types fn call deep$ guards$ ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (pseudo-term-listp inputs)
                             (atj-type-listp types)
                             (symbolp fn)
                             (pseudo-termp call)
                             (booleanp deep$)
                             (booleanp guards$)
                             (ctxp ctx))))
 (declare (xargs :guard (= (len types) (len inputs))))
 (let ((__function__ 'atj-process-test-inputs))
   (declare (ignorable __function__))
   (b* (((when (endp inputs)) (value nil))
        ((mv erp test-input state)
         (atj-process-test-input (car inputs)
                                 (car types)
                                 fn call deep$ guards$ ctx state))
        ((when erp) (mv t nil state))
        ((er test-inputs)
         (atj-process-test-inputs (cdr inputs)
                                  (cdr types)
                                  fn call deep$ guards$ ctx state)))
     (value (cons test-input test-inputs)))))

Theorem: atj-test-value-listp-of-atj-process-test-inputs.test-inputs

(defthm atj-test-value-listp-of-atj-process-test-inputs.test-inputs
  (b* (((mv ?erp ?test-inputs acl2::?state)
        (atj-process-test-inputs
             inputs
             types fn call deep$ guards$ ctx state)))
    (atj-test-value-listp test-inputs))
  :rule-classes :rewrite)