INTERN-IN-PACKAGE-OF-SYMBOL

create a symbol with a given name
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|