		Search-engine friendly clone of the ACL2 documentation.

Atj-test-structures

Atj-test-value-ACL2-list

Lift atj-test-value-ACL2 to lists.

Signature
(atj-test-value-acl2-list values) → test-values
Arguments: values — Guard (true-listp values).
Returns: test-values — Type (atj-test-value-listp test-values).

Definitions and Theorems

Function: atj-test-value-acl2-list

(defun atj-test-value-acl2-list (values)
  (declare (xargs :guard (true-listp values)))
  (let ((__function__ 'atj-test-value-acl2-list))
    (declare (ignorable __function__))
    (cond ((endp values) nil)
          (t (cons (atj-test-value-acl2 (car values))
                   (atj-test-value-acl2-list (cdr values)))))))

Theorem: atj-test-value-listp-of-atj-test-value-acl2-list

(defthm atj-test-value-listp-of-atj-test-value-acl2-list
  (b* ((test-values (atj-test-value-acl2-list values)))
    (atj-test-value-listp test-values))
  :rule-classes :rewrite)