Major Section: PROGRAMMING
(intern symbol-name symbol-package-name) returns a symbol with
symbol-name and the given
restrict Common Lisp's
intern so that the second argument is
either the symbol *main-lisp-package-name*, the value of that
constant, or is one of "ACL2", "ACL2-INPUT-CHANNEL",
"ACL2-OUTPUT-CHANNEL", or "KEYWORD".
intern is actually implemented as a macro that expands to
a call of a similar function whose second argument is a symbol.
:pe intern to see the definition, or
To see why is
intern so restricted consider
(intern "X" "P"). In particular, is it a symbol and if so,
what is its
symbol-package-name? One is tempted to say ``yes, it
is a symbol in the package
"P".'' But if package
not yet been defined, that would be premature because the imports to
the package are unknown. For example, if
"P" were introduced
(defpkg "P" '(LISP::X))then in Common Lisp
(symbol-package-name (intern "X" "P"))returns
The obvious restriction on
intern is that its second argument be
the name of a package known to ACL2. We cannot express such a
restriction (except, for example, by limiting it to those packages
known at some fixed time, as we do). Instead, we provide
intern-in-package-of-symbol which requires a ``witness symbol''
for the package instead of the package. The witness symbol is any
symbol (expressible in ACL2) and uniquely specifies a package
necessarily known to ACL2.