Major Section: EVENTS
Examples: (defconst *digits* '(0 1 2 3 4 5 6 7 8 9)) (defconst *n-digits* (the unsigned-byte (length *digits*)))where
General Form: (defconst name term doc-string)
nameis a symbol beginning and ending with the character
termis a variable-free term that is evaluated to determine the value of the constant, and
doc-stringis 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
(Implementation note: this is important for proper support of
undoing and redefinition.)