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.)
Major Section: EVENTS
Examples: (defconst *digits* '(0 1 2 3 4 5 6 7 8 9)) (defconst *n-digits* (the unsigned-byte (length *digits*)))whereGeneral Form: (defconst name term doc-string)
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.)