package prefix that is not restricted to symbols
Major Section:  OTHER


ACL2 !>(defpkg "FOO" nil)

Form:  ( DEFPKG "FOO" ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ACL2 !>'#!foo(a b)
ACL2 !>'#!foo(a #!acl2 b)
(FOO::A B)
ACL2 !>'#!foo(#!acl2 a b)
(A FOO::B)
ACL2 !>'#!foo(#!"ACL2" a b)
(A FOO::B)
ACL2 !>

The ACL2 reader supports the syntax #!pkg-name expr where pkg-name is a string or symbol that names a package known to ACL2. As illustrated above, this syntax nests as one might expect. In the special case that expr is a symbol, #!pkg-name expr is equivalent to pkg-name::expr.