Major Section: OTHER
Examples:ACL2 !>(defpkg "FOO" nil)
Summary Form: ( DEFPKG "FOO" ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) "FOO" ACL2 !>'#!foo(a b) (FOO::A FOO::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.
