		Search-engine friendly clone of the ACL2 documentation.

Atj-input-processing

Atj-process-test-input-jprim-values

Lift atj-process-test-input-jprim-value to lists.

Signature
(atj-process-test-input-jprim-values inputs type fn call ctx state) → (mv erp values state)
Arguments: inputs — Guard (pseudo-term-listp inputs).; type — Guard (primitive-typep type).; fn — Just for error messages.
Guard (symbolp fn).; call — Just for error messages.
Guard (pseudo-termp call).; ctx — Guard (ctxp ctx).

Definitions and Theorems

Function: atj-process-test-input-jprim-values

(defun atj-process-test-input-jprim-values
       (inputs type fn call ctx state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (pseudo-term-listp inputs)
                              (primitive-typep type)
                              (symbolp fn)
                              (pseudo-termp call)
                              (ctxp ctx))))
  (let ((__function__ 'atj-process-test-input-jprim-values))
    (declare (ignorable __function__))
    (b* (((when (endp inputs)) (value nil))
         ((cons input inputs) inputs)
         ((mv erp value state)
          (atj-process-test-input-jprim-value
               input type fn call ctx state))
         ((when erp) (mv erp nil state))
         ((er values)
          (atj-process-test-input-jprim-values
               inputs type fn call ctx state)))
      (value (cons value values)))))

Theorem: boolean-value-listp-of-atj-process-test-input-jprim-values.values

(defthm
  boolean-value-listp-of-atj-process-test-input-jprim-values.values
  (implies (primitive-type-case type :boolean)
           (b* (((mv ?erp ?values acl2::?state)
                 (atj-process-test-input-jprim-values
                      inputs type fn call ctx state)))
             (boolean-value-listp values)))
  :rule-classes :rewrite)

Theorem: char-value-listp-of-atj-process-test-input-jprim-values.values

(defthm
     char-value-listp-of-atj-process-test-input-jprim-values.values
  (implies (primitive-type-case type :char)
           (b* (((mv ?erp ?values acl2::?state)
                 (atj-process-test-input-jprim-values
                      inputs type fn call ctx state)))
             (char-value-listp values)))
  :rule-classes :rewrite)

Theorem: byte-value-listp-of-atj-process-test-input-jprim-values.values

(defthm
     byte-value-listp-of-atj-process-test-input-jprim-values.values
  (implies (primitive-type-case type :byte)
           (b* (((mv ?erp ?values acl2::?state)
                 (atj-process-test-input-jprim-values
                      inputs type fn call ctx state)))
             (byte-value-listp values)))
  :rule-classes :rewrite)

Theorem: short-value-listp-of-atj-process-test-input-jprim-values.values

(defthm
    short-value-listp-of-atj-process-test-input-jprim-values.values
  (implies (primitive-type-case type :short)
           (b* (((mv ?erp ?values acl2::?state)
                 (atj-process-test-input-jprim-values
                      inputs type fn call ctx state)))
             (short-value-listp values)))
  :rule-classes :rewrite)

Theorem: int-value-listp-of-atj-process-test-input-jprim-values.values

(defthm
      int-value-listp-of-atj-process-test-input-jprim-values.values
  (implies (primitive-type-case type :int)
           (b* (((mv ?erp ?values acl2::?state)
                 (atj-process-test-input-jprim-values
                      inputs type fn call ctx state)))
             (int-value-listp values)))
  :rule-classes :rewrite)

Theorem: long-value-listp-of-atj-process-test-input-jprim-values.values

(defthm
     long-value-listp-of-atj-process-test-input-jprim-values.values
  (implies (primitive-type-case type :long)
           (b* (((mv ?erp ?values acl2::?state)
                 (atj-process-test-input-jprim-values
                      inputs type fn call ctx state)))
             (long-value-listp values)))
  :rule-classes :rewrite)