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.
(include-book "std/util/defconsts" :dir :system)
(defconsts *foo* 1)
(defconsts (*foo*) 1)
(defconsts (*foo* *bar*) (mv 1 2))
(defconsts (*foo* *bar* &) (mv 1 2 3))
(defconsts (& *shell* state) (getenv$ "SHELL" state))
(defconsts (*hundred* state)
(mv-let (col state)
(fmt "Hello, world!" nil *standard-co* state nil)
(declare (ignore col))
(mv 100 state)))
(defconsts names body)
where names may be a single symbol or a list of n symbols, and
body is a form that returns n values.
Each symbol in names should either be:
- A "starred" name like *foo*,
- The name of a stobj (e.g., state), or
- The symbol &, which means "ignore this return value."
We introduce a defconst form that binds each starred name to the
corresponding value returned by body.
Defconst versus Defconsts
NOTE: defconsts differs from defconst in an important way. When you use these forms in a book:
This has some performance implications:
- Computations that take a long time but produce "small" results (e.g.,
checking the primality of a large number) might best be done as defconsts
to avoid repeating the computation.
- Computations that are fast but produce "large" results (e.g.,
(make-list 10000)), might best be done as defconst, to avoid storing
this large list in the certificate.