DEFCONST

define a constant
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).