Find a symbol with a given name in a package import list.
When denoting a symbol
via a package name
This function looks up a symbol, by name,
in a list of symbol that is meant to be a package import list.
We return the first symbol found, if any.
If none is found, we return
An import list in a package definition of an ACL2 environment will have symbols with unique names; will have unique package names; this will be formalized elsewhere. Under this condition, returning the first symbol found is as good as returning any symbol with that name in the list, since there can be at most one.
(defun import-lookup (name imports) (declare (xargs :guard (and (stringp name) (symbol-value-listp imports)))) (let ((__function__ 'import-lookup)) (declare (ignorable __function__)) (b* (((when (endp imports)) nil) (import (car imports)) ((when (equal name (symbol-value->name import))) (symbol-value-fix import))) (import-lookup name (cdr imports)))))
(defthm maybe-symbol-valuep-of-import-lookup (b* ((symbol? (import-lookup name imports))) (maybe-symbol-valuep symbol?)) :rule-classes :rewrite)
(defthm import-lookup-of-symbol-value-list-fix-imports (equal (import-lookup name (symbol-value-list-fix imports)) (import-lookup name imports)))
(defthm import-lookup-symbol-value-list-equiv-congruence-on-imports (implies (symbol-value-list-equiv imports imports-equiv) (equal (import-lookup name imports) (import-lookup name imports-equiv))) :rule-classes :congruence)