Lift atj-gen-shallow-symbol-field to lists.
(atj-gen-shallow-symbol-fields symbols) → fields
Function:
(defun atj-gen-shallow-symbol-fields (symbols) (declare (xargs :guard (symbol-listp symbols))) (let ((__function__ 'atj-gen-shallow-symbol-fields)) (declare (ignorable __function__)) (cond ((endp symbols) nil) (t (cons (atj-gen-shallow-symbol-field (car symbols)) (atj-gen-shallow-symbol-fields (cdr symbols)))))))
Theorem:
(defthm jfield-listp-of-atj-gen-shallow-symbol-fields (b* ((fields (atj-gen-shallow-symbol-fields symbols))) (jfield-listp fields)) :rule-classes :rewrite)