		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-quoted-constant-generation

Atj-gen-shallow-string-fields

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

Signature
(atj-gen-shallow-string-fields strings) → fields
Arguments: strings — Guard (string-listp strings).
Returns: fields — Type (jfield-listp fields).

Definitions and Theorems

Function: atj-gen-shallow-string-fields

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

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

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