		Search-engine friendly clone of the ACL2 documentation.

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.

Examples:

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

General form:

(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:

Results from defconsts are stored in the ACL2::certificate, while
Results from defconst are recomputed at include-book time.

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.