		Search-engine friendly clone of the ACL2 documentation.

Packages

Package-lookup

Look up a package in a list, by name.

Signature
(package-lookup name packages) → package?
Arguments: name — Guard (stringp name).; packages — Guard (package-listp packages).
Returns: package? — Type (package-optionp package?).

We return the first package in the list with the given name, if any. If there is none, we return nil.

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.

Definitions and Theorems

Function: package-lookup

(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)))))

Theorem: package-optionp-of-package-lookup

(defthm package-optionp-of-package-lookup
  (b* ((package? (package-lookup name packages)))
    (package-optionp package?))
  :rule-classes :rewrite)

Theorem: package-lookup-of-package-list-fix-packages

(defthm package-lookup-of-package-list-fix-packages
  (equal (package-lookup name (package-list-fix packages))
         (package-lookup name packages)))

Theorem: package-lookup-package-list-equiv-congruence-on-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)