Generate all the fields of the class for all the ACL2 packages.
(atj-gen-shallow-all-pkg-fields pkgs quoted-symbols quoted-symbols-by-pkg methods-by-pkg) → fields-by-pkg
We go through all the packages in
Function:
(defun atj-gen-shallow-all-pkg-fields (pkgs quoted-symbols quoted-symbols-by-pkg methods-by-pkg) (declare (xargs :guard (and (string-listp pkgs) (symbol-listp quoted-symbols) (string-symbollist-alistp quoted-symbols-by-pkg) (string-jmethodlist-alistp methods-by-pkg)))) (let ((__function__ 'atj-gen-shallow-all-pkg-fields)) (declare (ignorable __function__)) (b* (((when (endp pkgs)) nil) (pkg (car pkgs)) (first-fields (atj-gen-shallow-pkg-fields pkg quoted-symbols quoted-symbols-by-pkg methods-by-pkg)) (rest-fields (atj-gen-shallow-all-pkg-fields (cdr pkgs) quoted-symbols quoted-symbols-by-pkg methods-by-pkg))) (if (null first-fields) rest-fields (acons pkg first-fields rest-fields)))))
Theorem:
(defthm string-jfieldlist-alistp-of-atj-gen-shallow-all-pkg-fields (implies (string-listp pkgs) (b* ((fields-by-pkg (atj-gen-shallow-all-pkg-fields pkgs quoted-symbols quoted-symbols-by-pkg methods-by-pkg))) (string-jfieldlist-alistp fields-by-pkg))) :rule-classes :rewrite)