Defval
A replacement for defconst with xdoc integration.
Basic Example
(defval *defval-example-number*
:parents (defval)
:short "Example of a constant for @(see defval)."
:long "<p>This number is not very important.</p>"
(fib 5))
This is equivalent to just doing a defxdoc followed by a defconst, except that the :long string will be automatically extended
with the defining event for *defval-example-number*.
General Form
(defval *name*
[keyword options]
body ;; defining expression
[/// other events])
Option Default
:parents nil
:short nil
:long nil
:showdef t
:showval nil
:prepwork nil
The :parents, :short, and :long options are as in defxdoc. Typically you should specify at least :parents, perhaps
implicitly with ACL2::set-default-parents, to get bare-bones
documentation put into your manual in the right place.
The :showdef and :showval options control what kind of
documentation will be added to your :long section, if any. These options
are independent, i.e., you can say that you want either, both, or neither kinds
of automatic documentation.
When :showdef is enabled, which is the default, defval will
automatically extend your :long string with a the definition of the
constant. For instance, here's what this looks like for
*defval-example-number*:
Definition: *defval-example-number*
(defconst *defval-example-number* (fib 5))
In contrast, when :showval is enabled, defval will extend
:long with the value of your constant, e.g.,
Value:
8
The optional :prepwork argument can be used to put arbitrary events
before the constant. This could be used, for instance, to define functions
that are going to be used in the definition of the constant. These events will
be documented as in the usual defsection style.
The optional /// syntax is like that of define. After the
/// you can put related events that should come after the definition.
These events will be included in the documentation, as in defsection.
Warning about Large Constants
Either :showdef or :showval can cause problems when the
printed representation of your constant's definition or value is very large.
Trying to put huge values into the documentation could cause performance
problems when generating or viewing the manual.
This is much more likely to be a problem with :showval, since even very
small definitions like (make-list 100000) can produce large values.
Because of this, defval disables :showval disabled by default.
This is unlikely to be a problem for :showdef when you are writing your
own defval forms. However, if you are using make-event or other
macros to generate defval forms, you will need to be careful.
