Pkg-imports
List of symbols imported into a given package
Completion Axiom (completion-of-pkg-imports):
(equal (pkg-imports x)
(if (stringp x)
(pkg-imports x)
nil))
Guard for (pkg-imports x):
(stringp x)
(Pkg-imports pkg) returns a duplicate-free list of all symbols
imported into pkg, which should be the name of a package known to ACL2.
For example, suppose "MY-PKG" was created by
(defpkg "MY-PKG" '(ACL2::ABC LISP::CAR)).
Then (pkg-imports "MY-PKG") equals the list (ACL2::ABC
LISP::CAR).
If pkg is not a string, then (pkg-imports pkg) is nil. If
pkg is a string but not the name of a package known to ACL2, then the
value of the form (pkg-imports pkg) is unspecified, and its evaluation
will fail to yield a value. By ``the symbols imported into pkg'' we mean
the symbols imported into pkg by the defpkg event that introduced
pkg. There are no imports for built-in packages except for the
"ACL2" package, which imports the symbols in the list value of the
constant *common-lisp-symbols-from-main-lisp-package*. In particular,
this is the case for the "COMMON-LISP" package. Users familiar with
Common Lisp may find this surprising, since in actual Common Lisp
implementations it is often the case that many symbols in that package are
imported from other packages. However, ACL2 treats all symbols in the
constant *common-lisp-symbols-from-main-lisp-package* as having a symbol-package-name of "COMMON-LISP", as though they were not
imported. ACL2 admits a symbol imported into in the "COMMON-LISP"
package only if it belongs to that list: any attempt to read any other symbol
imported into the "COMMON-LISP" package, or to produce such a symbol
with intern$ or intern-in-package-of-symbol, will cause an
error.
The following axioms formalize properties of pkg-imports discussed
above (use :pe to view them).
symbol-package-name-intern-in-package-of-symbol
intern-in-package-of-symbol-is-identity
symbol-listp-pkg-imports
no-duplicatesp-pkg-imports
completion-of-pkg-imports
