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.

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