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*
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.