Major Section: EVENTS
Examples: (defconst *digits* '(0 1 2 3 4 5 6 7 8 9)) (defconst *n-digits* (the unsigned-byte (length *digits*))) General Form: (defconst name term doc-string)where
name is a symbol beginning and ending with the character *,
term is a variable-free term that is evaluated to determine the
value of the constant, and doc-string is an optional documentation
string (see doc-string).When a constant symbol is used as a term, ACL2 replaces it by its value; see term.
Note that defconst uses a ``safe mode'' to evaluate its form, in order
to avoids soundness issues but with an efficiency penalty (perhaps increasing
the evaluation time by several hundred percent). If efficiency is a concern,
or if for some reason you need the form to be evaluated without safe mode
(e.g., you are an advanced system hacker using trust tags to traffic in raw
Lisp code), consider using the macro defconst-fast instead, defined in
community book books/make-event/defconst-fast.lisp, for example:
(defconst-fast *x* (expensive-fn ...))A more general utility may be found in community book
books/tools/defconsts.lisp. Also using-tables-efficiently for an
analogous issue with table events.It may be of interest to note that defconst is implemented at the
lisp level using defparameter, as opposed to defconstant.
(Implementation note: this is important for proper support of
undoing and redefinition.)
We close with a technical remark, perhaps of interest only to users of
ACL2(h), the experimental extension of ACL2 that supports hash cons, function
memoization, and hash-table-based ``fast alists''; see hons-and-memoization.
For an event of the form (defconst *C* (quote OBJ)), i.e.,
(defconst *C* 'OBJ), then the value associated with *C* is OBJ;
that is, the value of *C* is eq to the actual object OBJ
occurring in the defconst form. So for example, if make-event is
used to generate such a defconst event, as it is in the two books
mentioned above, and OBJ is a fast alist (using ACL2(h)), then the value
of *C* is a fast alist. This guarantee disappears if the term in the
defconst form is not a quoted object, i.e., if it is not of the form
(quote OBJ).
