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, consider using the macro defconst-fast instead, defined in books/make-event/defconst-fast.lisp, for example:

(defconst-fast *x* (expensive-fn ...))
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.)