		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-quoted-constant-generation

Atj-gen-shallow-number-fields

Lift atj-gen-shallow-number-field to lists.

Signature
(atj-gen-shallow-number-fields numbers) → fields
Arguments: numbers — Guard (acl2-number-listp numbers).
Returns: fields — Type (jfield-listp fields).

Definitions and Theorems

Function: atj-gen-shallow-number-fields

(defun atj-gen-shallow-number-fields (numbers)
 (declare (xargs :guard (acl2-number-listp numbers)))
 (let ((__function__ 'atj-gen-shallow-number-fields))
   (declare (ignorable __function__))
   (cond ((endp numbers) nil)
         (t (cons (atj-gen-shallow-number-field (car numbers))
                  (atj-gen-shallow-number-fields (cdr numbers)))))))

Theorem: jfield-listp-of-atj-gen-shallow-number-fields

(defthm jfield-listp-of-atj-gen-shallow-number-fields
  (b* ((fields (atj-gen-shallow-number-fields numbers)))
    (jfield-listp fields))
  :rule-classes :rewrite)