Look up a package in a list, by name.
We return the first package in the list with the given name, if any.
If there is none, we return
When a list of packages represents all the package definitions in an ACL2 environment, the list will have unique package names; this will be formalized elsewhere. Under this condition, returning the first package found is as good as returning any package with that name in the list, since there can be at most one.
(defun package-lookup (name packages) (declare (xargs :guard (and (stringp name) (package-listp packages)))) (let ((__function__ 'package-lookup)) (declare (ignorable __function__)) (b* (((when (endp packages)) nil) (package (car packages)) ((when (equal name (package->name package))) (package-fix package))) (package-lookup name (cdr packages)))))
(defthm maybe-packagep-of-package-lookup (b* ((package? (package-lookup name packages))) (maybe-packagep package?)) :rule-classes :rewrite)
(defthm package-lookup-of-package-list-fix-packages (equal (package-lookup name (package-list-fix packages)) (package-lookup name packages)))
(defthm package-lookup-package-list-equiv-congruence-on-packages (implies (package-list-equiv packages packages-equiv) (equal (package-lookup name packages) (package-lookup name packages-equiv))) :rule-classes :congruence)