Sharp-dot-reader
Read-time evaluation of constants
Example:
ACL2 !>(defconst *a* '(a b c))
Summary
Form: ( DEFCONST *A* ...)
Rules: NIL
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
*A*
ACL2 !>(quote (1 2 #.*a* 3 4))
(1 2 (A B C) 3 4)
ACL2 !>
The ACL2 reader supports the syntax #.*a* where *a* was defined
by defconst. In this case, the reader treats #.*a* as though it
were reading the value of *a*. This feature can be useful in conjunction
with the use of evisc-table to abbreviate large constants, so that the
abbreviation can be read back in; see evisc-table.
Remarks.
(1) The ACL2 reader only supports `#.' as described above, unlike
Common Lisp. Older versions (preceding 3.5) used `#.' to abort, but that
functionality is now carried out by (a!); see a!. For a related
feature that only pops up one level, see p!.
(2) If you call certify-book on a book that contains a form
`#.*foo*', the *foo* must already be defined in the world in
which you issue the certify-book command. The reason is that
certify-book reads the entire book before evaluating its forms.
