• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Hons-and-memoization
    • Events
    • History
    • Parallelism
    • Programming
    • Start-here
    • Real
    • Debugging
    • Miscellaneous
      • Term
      • Ld
      • Hints
      • Type-set
      • Ordinals
      • ACL2-customization
      • With-prover-step-limit
      • With-prover-time-limit
      • Set-prover-step-limit
      • Local-incompatibility
      • Set-case-split-limitations
      • Subversive-recursions
      • Specious-simplification
      • Defsum
      • Oracle-timelimit
      • Thm
      • Defopener
      • Gcl
      • Case-split-limitations
      • Set-gc-strategy
      • Default-defun-mode
      • Top-level
      • Reader
        • Sharp-f-reader
        • Fancy-string-reader
        • Sharp-u-reader
        • Sharp-dot-reader
        • Backquote
        • Sharp-bang-reader
      • Ttags-seen
      • Adviser
      • Ttree
      • Abort-soft
      • Defsums
      • Gc$
      • With-timeout
      • Coi-debug::fail
      • Expander
      • Gc-strategy
      • Coi-debug::assert
      • Sin-cos
      • Def::doc
      • Syntax
      • Subversive-inductions
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Reader
• Packages

Sharp-bang-reader

Package prefix that is not restricted to symbols

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.