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