INTERN

create a new symbol in a given package
Major Section:  ACL2-BUILT-INS

(intern symbol-name symbol-package-name) returns a symbol with the given symbol-name and the given symbol-package-name. We 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". To avoid that restriction, see intern$.

In ACL2 intern is actually implemented as a macro that expands to a call of a similar function whose second argument is a symbol. Invoke :pe intern to see the definition, or see intern-in-package-of-symbol.

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 "P" has not yet been defined, that would be premature because the imports to the package are unknown. For example, if "P" were introduced with

(defpkg "P" '(LISP::X))
then in Common Lisp (symbol-package-name (intern "X" "P")) returns "LISP".

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.