Defconst
Define a constant
Examples:
(defconst *my-digits* '(0 1 2 3 4 5 6 7 8 9))
(defconst *len-my-digits* (the unsigned-byte (length *my-digits*)))
General Form:
(defconst name term)
where name is a symbol beginning and ending with the character *
and term is a variable-free term that is evaluated to determine the value
of the constant.
There are two restrictions on term aside from it being variable-free.
Both restrictions relate to ancestral uses of apply$ in term, i.e.,
uses of apply$ by term or any function that might be called during the
evaluation of term. First, only badged primitive functions may be
applied. See badge for a way to obtain the complete list of badged
primitives. Second, loop$ and lambda$ may not be used anywhere in
the ancestry of term. See ignored-attachment and
prohibition-of-loop$-and-lambda$ for more discussion.
When a constant symbol is used as a term, ACL2 replaces it by its
value; see term.
Note that defconst uses so-called 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, or if for some reason you need the form to be
evaluated without safe mode (e.g., you are an advanced system hacker using
trust tags to traffic in raw Lisp code), consider using defconsts
instead. Also see 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.)
We close with a technical remark, perhaps of interest only who make use of
the hons-enabled features of ACL2. For an event of the form
(defconst *C* (quote OBJ)), i.e., (defconst *C* 'OBJ), then the
value associated with *C* is OBJ; that is, the value of *C* is
eq to the actual object OBJ occurring in the defconst form.
So for example, if make-event is used to generate such a defconst
event, as it is in the two books mentioned above, and OBJ is a fast
alist (see fast-alists), then the value of *C* is a fast alist.
This guarantee disappears if the term in the defconst form is not a
quoted object, i.e., if it is not of the form (quote OBJ).
Subtopics
- Prohibition-of-loop$-and-lambda$
- Certain events do not allow loop$s or lambda$s
- Defval
- A replacement for defconst with xdoc integration.
- Ignored-attachment
- Why attachments are sometimes not used
- Defconsts
- An enhanced variant of defconst that lets you use state
and other ACL2::stobjs, and directly supports calling mv-returning functions to define multiple constants.
- Sharp-dot-reader
- Read-time evaluation of constants
