Major Section: ACL2-BUILT-INS
Completion Axiom (completion-of-intern-in-package-of-symbol):
(equal (intern-in-package-of-symbol x y)
(if (and (stringp x)
(symbolp y))
(intern-in-package-of-symbol x y)
nil))
Guard for (intern-in-package-of-symbol x y):
(and (stringp x) (symbolp y))
Intuitively, (intern-in-package-of-symbol x y) creates a symbol
with symbol-name x interned in the package containing y.
More precisely, suppose x is a string, y is a symbol with
symbol-package-name pkg and that the defpkg event creating pkg
had the list of symbols imports as the value of its second argument.
Then (intern-in-package-of-symbol x y) returns a symbol, ans, the
symbol-name of ans is x, and the symbol-package-name of ans
is pkg, unless x is the symbol-name of some member of imports
with symbol-package-name ipkg, in which case the
symbol-package-name of ans is ipkg. Because defpkg requires
that there be no duplications among the symbol-names of the
imports, intern-in-package-of-symbol is uniquely defined.
For example, suppose "MY-PKG" was created by
(defpkg "MY-PKG" '(ACL2::ABC LISP::CAR)).Let
w be 'my-pkg::witness. Observe that
(symbolp w) is t ; w is a symbol (symbol-name w) is "WITNESS" ; w's name is "WITNESS" (symbol-package-name w) is "MY-PKG" ; w is in the package "MY-PKG"The construction of
w illustrates one way to obtain a symbol in a given
package: write it down as a constant using the double-colon notation.But another way to obtain a symbol in a given package is to create it with
intern-in-package-of-symbol.
(intern-in-package-of-symbol "XYZ" w) is MY-PKG::XYZ (intern-in-package-of-symbol "ABC" w) is ACL2::ABC (intern-in-package-of-symbol "CAR" w) is LISP::CAR (intern-in-package-of-symbol "car" w) is MY-PKG::|car|
