Intern-in-package-of-symbol
Create a symbol with a given name
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|
Subtopics
- Intern-list
- Generate a list of symbols in some package.
- Std/basic/intern-in-package-of-symbol
- Lemmas about intern-in-package-of-symbol available in the
std/basic library.
