Major Section: OTHER
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* 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.
(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* 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.