Fancy (encapsulate nil ...) with a name and xdoc support.
... events and commentary ...)
:parents (parent1 parent2 ...)
:short "@(call foo) is like @(see bar), but better when..."
:long "<p>The main differences between @('foo') and @('bar') are ...</p>"
(defund foo (x) ...)
(local (in-theory (enable foo)))
(defthm foo-thm1 ...)
(defthm foo-thm2 ...)
"<p>NOTE: the next theorem is really useful, but we keep it disabled
because it gets too expensive when...</p>"
(defthmd foo-thm3 ...))
Note: this example might be better written as a ACL2::define,
which is much like a defsection but has additional features.
Like an encapsulate, a defsection introduces a new scope for
local events. This is often useful when you are trying to prove a
theorem that requires some lemmas: by proving the lemmas locally, you can
prevent them from affecting the rest of your book.
It is often useful to organize books into sections. There are a few minor
reasons you might prefer using defsection for this, instead of plain
encapsulates. For instance,
- It is easier to identify in the :pbt history, and
- It indents more nicely than encapsulate in a vanilla emacs.
But the main reasons to use defsection are its documentation features.
The definitions and theorems within a section can be automatically
included in the documentation page for that section, along with any running
commentary. This helps to avoid copying-and-pasting code into the manual, and
keeps it up-to-date as the code changes.
The :parents, :short, and :long keywords are optional. If
any of these keywords are provided, they will be used to introduce a defxdoc command; otherwise no documentation will be generated.
By default, the :long string you give will be automatically extended
with a "Definitions and Theorems" part that lists all of the (non-local,
non-redundant) definitions and theorems introduced in the section.
For instance, in the above example, the :long field would be extended
<h3>Definition and Theorems</h3>
<p>NOTE: the next theorem is really useful, but we keep it disabled
because it gets too expensive when...</p>
If you do not want this automatic documentation, you can turn it off with
If you want the section name to be the default parent for the encapsulated
events, then you can pass :set-as-default-parent t. Then (local
(xdoc::set-default-parents name)) will be inserted at the beginning of the
events, where "name" is the name of the section.
The :extension keyword allows you to say that this section is a
continuation of a previously introduced concept.
When :extension topic is provided, then topic must be the name of
a previously documented xdoc section, and you are not allowed to use
:parents or :short since the topic already exists. Note that whereas
topics can have multiple parents, you can only extend a single topic at a
The main purpose of an :extension section is to add additional
documentation, either via the :long string or via the automatic events and
commentary. The documentation obtained this way is just appended onto the
existing :long for the topic.
For example, say we have already defined the above foo section in some
"basic" book. We might then want to add some additional "advanced"
theorems about it in some other book. We could do this via:
"<p>Additional theorems are also available in the @('advanced') book. (We
don't include these in the basic book since they take a long time to
(defthm foo-thm4 ...)
(defthm foo-thm5 ...))
This will result in the commentary and definitions of foo-thm4 and
foo-thm5 being added onto the end of the documentation for foo.
- Throw away any keyword arguments and their values from a macro
- Get the value for a keyword argument like :foo value.