read-time evaluation of constants
Major Section:  OTHER


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.